PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun preserves fin 1 1 1 1

S,T:Type. (n:, f:(nS), g:(Sn). g o f = Id & f o g = Id) & (n:, f:(nT), g:(Tn). g o f = Id & f o g = Id) (n:, f:(nST), g:((ST)n). g o f = Id & f o g = Id)
By: GenUnivCD
Generated subgoal:

11. S: Type
2. T: Type
3. (n:, f:(nS), g:(Sn). g o f = Id & f o g = Id) & (n:, f:(nT), g:(Tn). g o f = Id & f o g = Id)
n:, f:(nST), g:((ST)n). g o f = Id & f o g = Id

About:
alluniverseimpliesandexistsfunctionnatural_numberequal