PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun preserves fin 1 1 1 1 1 1
1. S: Type
2. T: Type
3. n:
4. f:(nS), g:(Sn). g o f = Id & f o g = Id
5. n:, f:(nT), g:(Tn). g o f = Id nn & f o g = Id

n:, f:(nST), g:((ST)n). g o f = Id nn & f o g = Id
By:
Analyze 4
THEN
Analyze 5
Generated subgoal:

14. f: nS
5. g: Sn
6. g o f = Id & f o g = Id
7. n:, f:(nT), g:(Tn). g o f = Id & f o g = Id TT
n:, f:(nST), g:((ST)n). g o f = Id & f o g = Id (ST)ST

About:
existsfunctionnatural_numberandequaluniverse