defpred S₁[ set , set , set ] means ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( $2 = [[F,F1],t] & $1 = [[F1,F2],t1] & $3 = [[F,F2],(t1 `*` t)] );
deffunc H₁( set ) -> set = ($1 `1 ) `1 ;

A1: now

let x, y, z1, z2 be set ; :: thesis:
assume that
x in NatTrans A,B and
y in NatTrans A,B ; :: thesis:
assume S₁[x,y,z1] ; :: thesis:
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A2: y = [[F,F1],t] and
A3: x = [[F1,F2],t1] and
A4: z1 = [[F,F2],(t1 `*` t)] ;
assume S₁[x,y,z2] ; :: thesis:
then consider F', F1', F2' being Functor of A,B, t' being natural_transformation of F',F1', t1' being natural_transformation of F1',F2' such that
A5: y = [[F',F1'],t'] and
A6: x = [[F1',F2'],t1'] and
A7: z2 = [[F',F2'],(t1' `*` t')] ;
A8: t = t' by A2, A5, ZFMISC_1:33;
[F1,F2] = [F1',F2'] by A3, A6, ZFMISC_1:33;
then A9: F2 = F2' by ZFMISC_1:33;
A10: t1 = t1' by A3, A6, ZFMISC_1:33;
A11: [F,F1] = [F',F1'] by A2, A5, ZFMISC_1:33;
then F = F' by ZFMISC_1:33;
hence z1 = z2 by A4, A7, A11, A8, A10, A9, ZFMISC_1:33; :: thesis:

end;

A12: now

let x, y, z be set ; :: thesis:
assume that
A13: x in NatTrans A,B and
A14: y in NatTrans A,B ; :: thesis:
assume S₁[x,y,z] ; :: thesis:
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A15: y = [[F,F1],t] and
A16: x = [[F1,F2],t1] and
A17: z = [[F,F2],(t1 `*` t)] ;
A18: F1 is_naturally_transformable_to F2 by A13, A16, Th35;
F is_naturally_transformable_to F1 by A14, A15, Th35;
then F is_naturally_transformable_to F2 by A18, Th25;
hence z in NatTrans A,B by A17, Th35; :: thesis:

end;

consider m being PartFunc of , such that
A19: for x, y being set holds
( [x,y] in dom m iff ( x in NatTrans A,B & y in NatTrans A,B & ex z being set st S₁[x,y,z] ) ) and
A20: for x, y being set st [x,y] in dom m holds
S₁[x,y,m . x,y] from BINOP_1:sch 5(A12, A1);

A21: now

let t be Element of NatTrans A,B; :: thesis:
consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that
A22: t = [[F1,F2],s] and
F1 is_naturally_transformable_to F2 by Def16;
(t `1 ) `1 = [F1,F2] `1 by A22, MCART_1:7
.= F1 by MCART_1:7 ;
hence H₁(t) in Funct A,B by CAT_2:def 2; :: thesis:

end;

consider d being Function of NatTrans A,B, Funct A,B such that
A23: for t being Element of NatTrans A,B holds d . t = H₁(t) from FUNCT_2:sch 8(A21);
deffunc H₂( set ) -> set = ($1 `1 ) `2 ;

A24: now

let t be Element of NatTrans A,B; :: thesis:
consider F1, F2 being Functor of A,B, s being natural_transformation of F1,F2 such that
A25: t = [[F1,F2],s] and
F1 is_naturally_transformable_to F2 by Def16;
(t `1 ) `2 = [F1,F2] `2 by A25, MCART_1:7
.= F2 by MCART_1:7 ;
hence H₂(t) in Funct A,B by CAT_2:def 2; :: thesis:

end;

consider c being Function of NatTrans A,B, Funct A,B such that
A26: for t being Element of NatTrans A,B holds c . t = H₂(t) from FUNCT_2:sch 8(A24);
deffunc H₃( Element of Funct A,B) -> set = [[$1,$1],(id $1)];
A27: for F being Element of Funct A,B holds H₃(F) in NatTrans A,B by Def16;
consider i being Function of Funct A,B, NatTrans A,B such that
A28: for F being Element of Funct A,B holds i . F = H₃(F) from FUNCT_2:sch 8(A27);
set C = CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #);

A29: now

let F, F1, F2 be Functor of A,B; :: thesis:
let t be natural_transformation of F,F1; :: thesis:
let t1 be natural_transformation of F1,F2; :: thesis:
assume that
A30: F1 is_naturally_transformable_to F2 and
A31: F is_naturally_transformable_to F1 ; :: thesis:
A32: [[F,F1],t] in NatTrans A,B by A31, Th35;
A33: S₁[[[F1,F2],t1],[[F,F1],t],[[F,F2],(t1 `*` t)]] ;
[[F1,F2],t1] in NatTrans A,B by A30, Th35;
then [[[F1,F2],t1],[[F,F1],t]] in dom m by A19, A32, A33;
then consider F', F1', F2' being Functor of A,B, t' being natural_transformation of F',F1', t1' being natural_transformation of F1',F2' such that
A34: [[F,F1],t] = [[F',F1'],t'] and
A35: [[F1,F2],t1] = [[F1',F2'],t1'] and
A36: m . [[F1,F2],t1],[[F,F1],t] = [[F',F2'],(t1' `*` t')] by A20;
A37: t = t' by A34, ZFMISC_1:33;
[F1,F2] = [F1',F2'] by A35, ZFMISC_1:33;
then A38: F2 = F2' by ZFMISC_1:33;
A39: t1 = t1' by A35, ZFMISC_1:33;
A40: [F,F1] = [F',F1'] by A34, ZFMISC_1:33;
then F = F' by ZFMISC_1:33;
hence m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] by A36, A40, A37, A39, A38, ZFMISC_1:33; :: thesis:

end;

now

thus A41: for f, g being Element of the carrier' of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) holds
( [g,f] in dom the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) iff the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f ) :: thesis:

proof

assume [g,f] in dom the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) ; :: thesis:
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A44: f = [[F,F1],t] and
A45: g = [[F1,F2],t1] and
m . g,f = [[F,F2],(t1 `*` t)] by A20;
thus the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g = (g `1 ) `1 by A23
.= [F1,F2] `1 by A45, MCART_1:7
.= F1 by MCART_1:7
.= [F,F1] `2 by MCART_1:7
.= (f `1 ) `2 by A44, MCART_1:7
.= the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f by A26 ; :: thesis:

end;

assume A46: the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f ; :: thesis:
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A47: g = [[F1,F2],t] and
A48: F1 is_naturally_transformable_to F2 by Def16;
A49: F1 = [F1,F2] `1 by MCART_1:7
.= (g `1 ) `1 by A47, MCART_1:7
.= c . f by A23, A46
.= (f `1 ) `2 by A26
.= [F1',F2'] `2 by A42, MCART_1:7
.= F2' by MCART_1:7 ;
then reconsider t = t as natural_transformation of F2',F2 ;
m . [g,f] = [[F1',F2],(t `*` t')] by A29, A47, A48, A42, A43, A49;
hence [g,f] in dom the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) by A19, A47, A42, A49; :: thesis:

end;

thus for f, g being Element of the carrier' of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) st the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f holds
( the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g,f) = the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f & the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g,f) = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g ) :: thesis:

proof

let f, g be Element of the carrier' of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #); :: thesis:
consider F1', F2' being Functor of A,B, t' being natural_transformation of F1',F2' such that
A50: f = [[F1',F2'],t'] and
A51: F1' is_naturally_transformable_to F2' by Def16;
assume the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f ; :: thesis:
then [g,f] in dom m by A41;
then consider F, F1, F2 being Functor of A,B, t being natural_transformation of F,F1, t1 being natural_transformation of F1,F2 such that
A52: f = [[F,F1],t] and
A53: g = [[F1,F2],t1] and
A54: m . g,f = [[F,F2],(t1 `*` t)] by A20;
A55: [F,F1] = [F1',F2'] by A52, A50, ZFMISC_1:33;
then A56: F = F1' by ZFMISC_1:33;
A57: F1 = F2' by A55, ZFMISC_1:33;
consider F1', F2' being Functor of A,B, t' being natural_transformation of F1',F2' such that
A58: g = [[F1',F2'],t'] and
A59: F1' is_naturally_transformable_to F2' by Def16;
A60: [F1,F2] = [F1',F2'] by A53, A58, ZFMISC_1:33;
then A61: F2 = F2' by ZFMISC_1:33;
F1 = F1' by A60, ZFMISC_1:33;
then F is_naturally_transformable_to F2 by A51, A56, A57, A59, A61, Th25;
then reconsider x = [[F,F2],(t1 `*` t)] as Element of NatTrans A,B by Th35;
thus the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g,f) = (x `1 ) `1 by A23, A54
.= [F,F2] `1 by MCART_1:7
.= F by MCART_1:7
.= [F,F1] `1 by MCART_1:7
.= ([[F,F1],t] `1 ) `1 by MCART_1:7
.= the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f by A23, A52 ; :: thesis:
thus the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g,f) = (x `1 ) `2 by A26, A54
.= [F,F2] `2 by MCART_1:7
.= F2 by MCART_1:7
.= [F1,F2] `2 by MCART_1:7
.= ([[F1,F2],t1] `1 ) `2 by MCART_1:7
.= the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g by A26, A53 ; :: thesis:

end;

thus for f, g, h being Element of the carrier' of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) st the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . h = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g & the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f holds
the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . h,(the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g,f) = the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . h,g),f :: thesis:

proof

let f, g, h be Element of the carrier' of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #); :: thesis:
reconsider f' = f, g' = g, h' = h as Element of NatTrans A,B ;
assume that
A62: the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . h = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g and
A63: the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g = the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f ; :: thesis:
[g',f'] in dom m by A41, A63;
then consider F1, F1', F2 being Functor of A,B, t1 being natural_transformation of F1,F1', t2 being natural_transformation of F1',F2 such that
A64: f' = [[F1,F1'],t1] and
A65: g' = [[F1',F2],t2] and
A66: m . g',f' = [[F1,F2],(t2 `*` t1)] by A20;
[h',g'] in dom m by A41, A62;
then consider F2', F3, F3' being Functor of A,B, t2' being natural_transformation of F2',F3, t3 being natural_transformation of F3,F3' such that
A67: g' = [[F2',F3],t2'] and
A68: h' = [[F3,F3'],t3] and
m . h',g' = [[F2',F3'],(t3 `*` t2')] by A20;
A69: [F2',F3] = [F1',F2] by A65, A67, ZFMISC_1:33;
then A70: g' = [[F1',F3],t2] by A65, ZFMISC_1:33;
reconsider t2 = t2 as natural_transformation of F1',F3 by A69, ZFMISC_1:33;
A71: F2 = F3 by A69, ZFMISC_1:33;
then A72: F1' is_naturally_transformable_to F3 by A65, Th35;
A73: F3 is_naturally_transformable_to F3' by A68, Th35;
then A74: F1' is_naturally_transformable_to F3' by A72, Th25;
A75: F1 is_naturally_transformable_to F1' by A64, Th35;
then F1 is_naturally_transformable_to F3 by A72, Th25;
hence the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . h,(the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g,f) = [[F1,F3'],(t3 `*` (t2 `*` t1))] by A29, A66, A68, A71, A73
.= [[F1,F3'],((t3 `*` t2) `*` t1)] by A75, A72, A73, Th28
.= m . [[[F1',F3'],(t3 `*` t2)],f'] by A29, A64, A75, A74
.= the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . h,g),f by A29, A68, A70, A72, A73 ;
:: thesis:

end;

let b be Element of ; :: thesis:
reconsider F = b as Functor of A,B by CAT_2:def 2;
reconsider s = [[F,F],(id F)] as Element of NatTrans A,B by Def16;
A76: the Id of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . b = [[F,F],(id F)] by A28;
hence the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Id of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . b) = (s `1 ) `1 by A23
.= [F,F] `1 by MCART_1:7
.= b by MCART_1:7 ;
:: thesis:
thus the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Id of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . b) = (s `1 ) `2 by A26, A76
.= [F,F] `2 by MCART_1:7
.= b by MCART_1:7 ; :: thesis:
thus for f being Element of the carrier' of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) st the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f = b holds
the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Id of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . b),f = f :: thesis:

proof

let f be Element of the carrier' of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #); :: thesis:
reconsider f' = f as Element of NatTrans A,B ;
assume A77: the Target of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . f = b ; :: thesis:
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A78: f' = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def16;
A79: F2 = [F1,F2] `2 by MCART_1:7
.= (f' `1 ) `2 by A78, MCART_1:7
.= F by A26, A77 ;
then reconsider t = t as natural_transformation of F1,F ;
S₁[s,f',[[F1,F],((id F) `*` t)]] by A78, A79;
then [s,f'] in dom m by A19;
then [(i . F),f'] in dom m by A28;
then consider F', F1', F2' being Functor of A,B, t' being natural_transformation of F',F1', t1' being natural_transformation of F1',F2' such that
A80: f' = [[F',F1'],t'] and
A81: i . F = [[F1',F2'],t1'] and
A82: m . (i . F),f' = [[F',F2'],(t1' `*` t')] by A20;
A83: i . F = [[F,F],(id F)] by A28;
then A84: t1' = id F by A81, ZFMISC_1:33;
A85: [F1',F2'] = [F,F] by A81, A83, ZFMISC_1:33;
then A86: F1' = F by ZFMISC_1:33;
A87: F2' = F by A85, ZFMISC_1:33;
F' is_naturally_transformable_to F1' by A80, Th35;
hence the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . (the Id of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . b),f = f by A80, A82, A84, A86, A87, Th26; :: thesis:

end;

let g be Element of the carrier' of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #); :: thesis:
reconsider g' = g as Element of NatTrans A,B ;
assume A88: the Source of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g = b ; :: thesis:
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A89: g' = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def16;
A90: F1 = [F1,F2] `1 by MCART_1:7
.= (g' `1 ) `1 by A89, MCART_1:7
.= F by A23, A88 ;
then reconsider t = t as natural_transformation of F,F2 ;
S₁[g',s,[[F,F2],(t `*` (id F))]] by A89, A90;
then [g',s] in dom m by A19;
then [g',(i . F)] in dom m by A28;
then consider F', F1', F2' being Functor of A,B, t' being natural_transformation of F',F1', t1' being natural_transformation of F1',F2' such that
A91: i . F = [[F',F1'],t'] and
A92: g' = [[F1',F2'],t1'] and
A93: m . g',(i . F) = [[F',F2'],(t1' `*` t')] by A20;
A94: i . F = [[F,F],(id F)] by A28;
then A95: t' = id F by A91, ZFMISC_1:33;
A96: [F',F1'] = [F,F] by A91, A94, ZFMISC_1:33;
then A97: F1' = F by ZFMISC_1:33;
A98: F' = F by A96, ZFMISC_1:33;
F1' is_naturally_transformable_to F2' by A92, Th35;
hence the Comp of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . g,(the Id of CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) . b) = g by A92, A93, A95, A97, A98, Th26; :: thesis:

end;

then reconsider C = CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #) as strict Category by CAT_1:def 8;
take C ; :: thesis:
thus ( the carrier of C = Funct A,B & the carrier' of C = NatTrans A,B ) ; :: thesis:
thus for f being Morphism of holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) by A23, A26; :: thesis:
thus for f, g being Morphism of st dom g = cod f holds
[g,f] in dom the Comp of C :: thesis:

proof

let f, g be Morphism of ; :: thesis:
assume A99: dom g = cod f ; :: thesis:
consider F1', F2' being Functor of A,B, t' being natural_transformation of F1',F2' such that
A100: g = [[F1',F2'],t'] and
F1' is_naturally_transformable_to F2' by Def16;
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A101: f = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def16;
A102: F2 = [F1,F2] `2 by MCART_1:7
.= ([[F1,F2],t] `1 ) `2 by MCART_1:7
.= cod f by A26, A101
.= ([[F1',F2'],t'] `1 ) `1 by A23, A100, A99
.= [F1',F2'] `1 by MCART_1:7
.= F1' by MCART_1:7 ;
then reconsider t' = t' as natural_transformation of F2,F2' ;
S₁[g,f,[[F1,F2'],(t' `*` t)]] by A101, A100, A102;
hence [g,f] in dom the Comp of C by A19; :: thesis:

end;

thus for f, g being Morphism of st [g,f] in dom the Comp of C holds
ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) :: thesis:

proof

let f, g be Morphism of ; :: thesis:
assume [g,f] in dom the Comp of C ; :: thesis:
then ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . g,f = [[F,F2],(t1 `*` t)] ) by A20;
hence ex F, F1, F2 being Functor of A,B ex t being natural_transformation of F,F1 ex t1 being natural_transformation of F1,F2 st
( f = [[F,F1],t] & g = [[F1,F2],t1] & the Comp of C . [g,f] = [[F,F2],(t1 `*` t)] ) ; :: thesis:

end;

let a be Object of ; :: thesis:
let F be Functor of A,B; :: thesis:
assume F = a ; :: thesis:
hence id a = [[F,F],(id F)] by A28; :: thesis: