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 F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A5: y = [[F9,F19],t9] and
A6: x = [[F19,F29],t19] and
A7: z2 = [[F9,F29],(t19 `*` t9)] ;
A8: t = t9 by A2, A5, ZFMISC_1:33;
[F1,F2] = [F19,F29] by A3, A6, ZFMISC_1:33;
then A9: F2 = F29 by ZFMISC_1:33;
A10: t1 = t19 by A3, A6, ZFMISC_1:33;
A11: [F,F1] = [F9,F19] by A2, A5, ZFMISC_1:33;
then F = F9 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 [:(NatTrans A,B),(NatTrans A,B):],(NatTrans A,B) 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 F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A34: [[F,F1],t] = [[F9,F19],t9] and
A35: [[F1,F2],t1] = [[F19,F29],t19] and
A36: m . [[F1,F2],t1],[[F,F1],t] = [[F9,F29],(t19 `*` t9)] by A20;
A37: t = t9 by A34, ZFMISC_1:33;
[F1,F2] = [F19,F29] by A35, ZFMISC_1:33;
then A38: F2 = F29 by ZFMISC_1:33;
A39: t1 = t19 by A35, ZFMISC_1:33;
A40: [F,F1] = [F9,F19] by A34, ZFMISC_1:33;
then F = F9 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
.= [F19,F29] `2 by A42, MCART_1:7
.= F29 by MCART_1:7 ;
then reconsider t = t as natural_transformation of F29,F2 ;
m . [g,f] = [[F19,F2],(t `*` t9)] 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 F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A50: f = [[F19,F29],t9] and
A51: F19 is_naturally_transformable_to F29 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] = [F19,F29] by A52, A50, ZFMISC_1:33;
then A56: F = F19 by ZFMISC_1:33;
A57: F1 = F29 by A55, ZFMISC_1:33;
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A58: g = [[F19,F29],t9] and
A59: F19 is_naturally_transformable_to F29 by Def16;
A60: [F1,F2] = [F19,F29] by A53, A58, ZFMISC_1:33;
then A61: F2 = F29 by ZFMISC_1:33;
F1 = F19 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 f9 = f, g9 = g, h9 = 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:
[g9,f9] in dom m by A41, A63;
then consider F1, F19, F2 being Functor of A,B, t1 being natural_transformation of F1,F19, t2 being natural_transformation of F19,F2 such that
A64: f9 = [[F1,F19],t1] and
A65: g9 = [[F19,F2],t2] and
A66: m . g9,f9 = [[F1,F2],(t2 `*` t1)] by A20;
[h9,g9] in dom m by A41, A62;
then consider F29, F3, F39 being Functor of A,B, t29 being natural_transformation of F29,F3, t3 being natural_transformation of F3,F39 such that
A67: g9 = [[F29,F3],t29] and
A68: h9 = [[F3,F39],t3] and
m . h9,g9 = [[F29,F39],(t3 `*` t29)] by A20;
A69: [F29,F3] = [F19,F2] by A65, A67, ZFMISC_1:33;
then A70: g9 = [[F19,F3],t2] by A65, ZFMISC_1:33;
reconsider t2 = t2 as natural_transformation of F19,F3 by A69, ZFMISC_1:33;
A71: F2 = F3 by A69, ZFMISC_1:33;
then A72: F19 is_naturally_transformable_to F3 by A65, Th35;
A73: F3 is_naturally_transformable_to F39 by A68, Th35;
then A74: F19 is_naturally_transformable_to F39 by A72, Th25;
A75: F1 is_naturally_transformable_to F19 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,F39],(t3 `*` (t2 `*` t1))] by A29, A66, A68, A71, A73
.= [[F1,F39],((t3 `*` t2) `*` t1)] by A75, A72, A73, Th28
.= m . [[[F19,F39],(t3 `*` t2)],f9] 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 CatStr(# (Funct A,B),(NatTrans A,B),d,c,m,i #); :: 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 f9 = 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: f9 = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def16;
A79: F2 = [F1,F2] `2 by MCART_1:7
.= (f9 `1 ) `2 by A78, MCART_1:7
.= F by A26, A77 ;
then reconsider t = t as natural_transformation of F1,F ;
S₁[s,f9,[[F1,F],((id F) `*` t)]] by A78, A79;
then [s,f9] in dom m by A19;
then [(i . F),f9] in dom m by A28;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A80: f9 = [[F9,F19],t9] and
A81: i . F = [[F19,F29],t19] and
A82: m . (i . F),f9 = [[F9,F29],(t19 `*` t9)] by A20;
A83: i . F = [[F,F],(id F)] by A28;
then A84: t19 = id F by A81, ZFMISC_1:33;
A85: [F19,F29] = [F,F] by A81, A83, ZFMISC_1:33;
then A86: F19 = F by ZFMISC_1:33;
A87: F29 = F by A85, ZFMISC_1:33;
F9 is_naturally_transformable_to F19 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 g9 = 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: g9 = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def16;
A90: F1 = [F1,F2] `1 by MCART_1:7
.= (g9 `1 ) `1 by A89, MCART_1:7
.= F by A23, A88 ;
then reconsider t = t as natural_transformation of F,F2 ;
S₁[g9,s,[[F,F2],(t `*` (id F))]] by A89, A90;
then [g9,s] in dom m by A19;
then [g9,(i . F)] in dom m by A28;
then consider F9, F19, F29 being Functor of A,B, t9 being natural_transformation of F9,F19, t19 being natural_transformation of F19,F29 such that
A91: i . F = [[F9,F19],t9] and
A92: g9 = [[F19,F29],t19] and
A93: m . g9,(i . F) = [[F9,F29],(t19 `*` t9)] by A20;
A94: i . F = [[F,F],(id F)] by A28;
then A95: t9 = id F by A91, ZFMISC_1:33;
A96: [F9,F19] = [F,F] by A91, A94, ZFMISC_1:33;
then A97: F19 = F by ZFMISC_1:33;
A98: F9 = F by A96, ZFMISC_1:33;
F19 is_naturally_transformable_to F29 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 C holds
( dom f = (f `1 ) `1 & cod f = (f `1 ) `2 ) by A23, A26; :: thesis:
thus for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C :: thesis:

proof

let f, g be Morphism of C; :: thesis:
assume A99: dom g = cod f ; :: thesis:
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A100: g = [[F19,F29],t9] and
F19 is_naturally_transformable_to F29 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
.= ([[F19,F29],t9] `1 ) `1 by A23, A100, A99
.= [F19,F29] `1 by MCART_1:7
.= F19 by MCART_1:7 ;
then reconsider t9 = t9 as natural_transformation of F2,F29 ;
S₁[g,f,[[F1,F29],(t9 `*` 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 C 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 C; :: 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 C; :: thesis:
let F be Functor of A,B; :: thesis:
assume F = a ; :: thesis:
hence id a = [[F,F],(id F)] by A28; :: thesis: