defpred S₁[ object , object , object ] 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₁( object ) -> object = ($1 `1) `1 ;

A1: now :: thesis: for x, y, z1, z2 being object st x in NatTrans (A,B) & y in NatTrans (A,B) & S₁[x,y,z1] & S₁[x,y,z2] holds
z1 = z2

let x, y, z1, z2 be object ; :: thesis: ( x in NatTrans (A,B) & y in NatTrans (A,B) & S₁[x,y,z1] & S₁[x,y,z2] implies z1 = z2 )
assume that
x in NatTrans (A,B) and
y in NatTrans (A,B) ; :: thesis: ( S₁[x,y,z1] & S₁[x,y,z2] implies z1 = z2 )
assume S₁[x,y,z1] ; :: thesis: ( S₁[x,y,z2] implies z1 = z2 )
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: z1 = z2
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, XTUPLE_0:1;
[F1,F2] = [F19,F29] by A3, A6, XTUPLE_0:1;
then A9: F2 = F29 by XTUPLE_0:1;
A10: t1 = t19 by A3, A6, XTUPLE_0:1;
A11: [F,F1] = [F9,F19] by A2, A5, XTUPLE_0:1;
then F = F9 by XTUPLE_0:1;
hence z1 = z2 by A4, A7, A11, A8, A10, A9, XTUPLE_0:1; :: thesis: verum

end;

A12: now :: thesis: for x, y, z being object st x in NatTrans (A,B) & y in NatTrans (A,B) & S₁[x,y,z] holds
z in NatTrans (A,B)

let x, y, z be object ; :: thesis: ( x in NatTrans (A,B) & y in NatTrans (A,B) & S₁[x,y,z] implies z in NatTrans (A,B) )
assume that
A13: x in NatTrans (A,B) and
A14: y in NatTrans (A,B) ; :: thesis: ( S₁[x,y,z] implies z in NatTrans (A,B) )
assume S₁[x,y,z] ; :: thesis: z in NatTrans (A,B)
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, Th28;
F is_naturally_transformable_to F1 by A14, A15, Th28;
hence z in NatTrans (A,B) by A17, Th28, A18, Th19; :: thesis: verum

end;

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

A21: now :: thesis: for t being Element of NatTrans (A,B) holds H₁(t) in Funct (A,B)

let t be Element of NatTrans (A,B); :: thesis: H₁(t) in Funct (A,B)
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 Def15;
(t `1) `1 = [F1,F2] `1 by A22
.= F1 ;
hence H₁(t) in Funct (A,B) by CAT_2:def 2; :: thesis: verum

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 ) -> object = ($1 `1) `2 ;

A24: now :: thesis: for t being Element of NatTrans (A,B) holds H₂(t) in Funct (A,B)

let t be Element of NatTrans (A,B); :: thesis: H₂(t) in Funct (A,B)
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 Def15;
(t `1) `2 = [F1,F2] `2 by A25
.= F2 ;
hence H₂(t) in Funct (A,B) by CAT_2:def 2; :: thesis: verum

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)) -> object = [[$1,$1],(id $1)];
A27: for F being Element of Funct (A,B) holds H₃(F) in NatTrans (A,B) by Def15;
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 #);

A29: now :: thesis: for F, F1, F2 being Functor of A,B
for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]

let F, F1, F2 be Functor of A,B; :: thesis: for t being natural_transformation of F,F1
for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]
let t be natural_transformation of F,F1; :: thesis: for t1 being natural_transformation of F1,F2 st F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 holds
m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]
let t1 be natural_transformation of F1,F2; :: thesis: ( F1 is_naturally_transformable_to F2 & F is_naturally_transformable_to F1 implies m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] )
assume that
A30: F1 is_naturally_transformable_to F2 and
A31: F is_naturally_transformable_to F1 ; :: thesis: m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)]
A32: [[F,F1],t] in NatTrans (A,B) by A31, Th28;
A33: S₁[[[F1,F2],t1],[[F,F1],t],[[F,F2],(t1 `*` t)]] ;
[[F1,F2],t1] in NatTrans (A,B) by A30, Th28;
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, A19, A32, A33;
A37: t = t9 by A34, XTUPLE_0:1;
[F1,F2] = [F19,F29] by A35, XTUPLE_0:1;
then A38: F2 = F29 by XTUPLE_0:1;
A39: t1 = t19 by A35, XTUPLE_0:1;
A40: [F,F1] = [F9,F19] by A34, XTUPLE_0:1;
then F = F9 by XTUPLE_0:1;
hence m . [[[F1,F2],t1],[[F,F1],t]] = [[F,F2],(t1 `*` t)] by A36, A40, A37, A39, A38, XTUPLE_0:1; :: thesis: verum

end;

A41: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is Category-like

proof

let f, g be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def 6 :: thesis: ( ( not [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) or dom g = cod f ) & ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ) )
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A42: f = [[F19,F29],t9] and
A43: F19 is_naturally_transformable_to F29 by Def15;
thus ( [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) implies dom g = cod f ) :: thesis: ( not dom g = cod f or [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) )

proof

assume [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ; :: thesis: dom g = cod f
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 dom g = (g `1) `1 by A23
.= [F1,F2] `1 by A45
.= [F,F1] `2
.= (f `1) `2 by A44
.= cod f by A26 ; :: thesis: verum

end;

assume A46: dom g = cod f ; :: thesis: [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #)
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 Def15;
A49: F1 = [F1,F2] `1
.= (g `1) `1 by A47
.= c . f by A23, A46
.= (f `1) `2 by A26
.= [F19,F29] `2 by A42
.= F29 ;
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 proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A19, A47, A42, A49; :: thesis: verum

end;

A50: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is transitive

proof

let f, g be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def 7 :: thesis: ( not dom g = cod f or ( dom (g (*) f) = dom f & cod (g (*) f) = cod g ) )
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A51: f = [[F19,F29],t9] and
A52: F19 is_naturally_transformable_to F29 by Def15;
assume dom g = cod f ; :: thesis: ( dom (g (*) f) = dom f & cod (g (*) f) = cod g )
then A53: [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
A54: f = [[F,F1],t] and
A55: g = [[F1,F2],t1] and
A56: m . (g,f) = [[F,F2],(t1 `*` t)] by A20;
A57: m . (g,f) = g (*) f by A53, CAT_1:def 1;
A58: [F,F1] = [F19,F29] by A54, A51, XTUPLE_0:1;
then A59: F = F19 by XTUPLE_0:1;
A60: F1 = F29 by A58, XTUPLE_0:1;
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A61: g = [[F19,F29],t9] and
A62: F19 is_naturally_transformable_to F29 by Def15;
A63: [F1,F2] = [F19,F29] by A55, A61, XTUPLE_0:1;
then A64: F2 = F29 by XTUPLE_0:1;
F1 = F19 by A63, XTUPLE_0:1;
then reconsider x = [[F,F2],(t1 `*` t)] as Element of NatTrans (A,B) by Th28, A52, A59, A60, A62, A64, Th19;
thus dom (g (*) f) = (x `1) `1 by A23, A56, A57
.= [F,F2] `1
.= ([[F,F1],t] `1) `1
.= dom f by A23, A54 ; :: thesis: cod (g (*) f) = cod g
thus cod (g (*) f) = (x `1) `2 by A26, A56, A57
.= [F,F2] `2
.= ([[F1,F2],t1] `1) `2
.= cod g by A26, A55 ; :: thesis: verum

end;

A65: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is associative

proof

A66: for f, g being Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( [g,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) iff dom g = cod f ) by A41;
let f, g, h be Element of the carrier' of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def 8 :: thesis: ( not dom h = cod g or not dom g = cod f or h (*) (g (*) f) = (h (*) g) (*) f )
reconsider f9 = f, g9 = g, h9 = h as Element of NatTrans (A,B) ;
assume that
A67: dom h = cod g and
A68: dom g = cod f ; :: thesis: h (*) (g (*) f) = (h (*) g) (*) f
[g9,f9] in dom m by A41, A68;
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
A69: f9 = [[F1,F19],t1] and
A70: g9 = [[F19,F2],t2] and
A71: m . (g9,f9) = [[F1,F2],(t2 `*` t1)] by A20;
[h9,g9] in dom m by A41, A67;
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
A72: g9 = [[F29,F3],t29] and
A73: h9 = [[F3,F39],t3] and
m . (h9,g9) = [[F29,F39],(t3 `*` t29)] by A20;
A74: [F29,F3] = [F19,F2] by A70, A72, XTUPLE_0:1;
then A75: g9 = [[F19,F3],t2] by A70, XTUPLE_0:1;
reconsider t2 = t2 as natural_transformation of F19,F3 by A74, XTUPLE_0:1;
A76: F2 = F3 by A74, XTUPLE_0:1;
then A77: F19 is_naturally_transformable_to F3 by A70, Th28;
A78: F3 is_naturally_transformable_to F39 by A73, Th28;
then A79: F19 is_naturally_transformable_to F39 by A77, Th19;
A80: F1 is_naturally_transformable_to F19 by A69, Th28;
then A81: F1 is_naturally_transformable_to F3 by A77, Th19;
A82: h (*) g = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,g) by A66, A67, CAT_1:def 1;
A83: dom (h (*) g) = dom g by A50, A67;
A84: g (*) f = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (g,f) by A66, A68, CAT_1:def 1;
cod (g (*) f) = cod g by A50, A68;
hence h (*) (g (*) f) = the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,( the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (g,f))) by A84, A66, A67, CAT_1:def 1
.= [[F1,F39],(t3 `*` (t2 `*` t1))] by A29, A71, A73, A76, A78, A81
.= [[F1,F39],((t3 `*` t2) `*` t1)] by A80, A77, A78, Th22
.= m . [[[F19,F39],(t3 `*` t2)],f9] by A29, A69, A80, A79
.= the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (( the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) . (h,g)),f) by A29, A73, A75, A77, A78
.= (h (*) g) (*) f by A83, A82, A66, A68, CAT_1:def 1 ;
:: thesis: verum

end;

A85: CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is reflexive

proof

let b be Element of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def 9 :: thesis: not Hom (b,b) = {}
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 Def15;
reconsider s = s as Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ;
A86: dom s = ([[F,F],(id F)] `1) `1 by A23
.= F ;
cod s = ([[F,F],(id F)] `1) `2 by A26
.= F ;
then s in Hom (b,b) by A86;
hence Hom (b,b) <> {} ; :: thesis: verum

end;

A87: for a being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #)
for F being Functor of A,B st a = F holds
for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )

proof

let a be Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: thesis: for F being Functor of A,B st a = F holds
for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
let F be Functor of A,B; :: thesis: ( a = F implies for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) )
assume A88: a = F ; :: thesis: for m being Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) st m = [[F,F],(id F)] holds
for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) )
let ii be Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: thesis: ( ii = [[F,F],(id F)] implies for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) ) )
assume A89: ii = [[F,F],(id F)] ; :: thesis: for b being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
let b be Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: thesis: ( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f ) )
reconsider s = [[F,F],(id F)] as Element of NatTrans (A,B) by Def15;
A90: F in Funct (A,B) by CAT_2:def 2;
then A91: i . F = [[F,F],(id F)] by A28;
thus ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) ii = f ) :: thesis: ( Hom (b,a) <> {} implies for f being Morphism of b,a holds ii (*) f = f )

proof

assume A92: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds f (*) ii = f
let f be Morphism of a,b; :: thesis: f (*) ii = f
reconsider f9 = f as Element of NatTrans (A,B) ;
A93: dom f = a by A92, CAT_1:5;
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A94: f9 = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def15;
A95: F1 = [F1,F2] `1
.= (f9 `1) `1 by A94
.= dom f by A23
.= F by A92, A88, CAT_1:5 ;
then reconsider t = t as natural_transformation of F,F2 ;
S<sub>1</sub>[f9,s,[[F,F2],(t `*` (id F))]] by A94, A95;
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
A96: i . F = [[F9,F19],t9] and
A97: f9 = [[F19,F29],t19] and
A98: m . (f9,(i . F)) = [[F9,F29],(t19 `*` t9)] by A20, A91, A19;
A99: [F9,F19] = [F,F] by A96, A91, XTUPLE_0:1;
then A100: F9 = F by XTUPLE_0:1;
A101: F19 = F by A99, XTUPLE_0:1;
A102: F19 is_naturally_transformable_to F29 by A97, Th28;
A103: F29 = ([[F19,F29],t19] `1) `2
.= ([[F1,F2],t] `1) `2 by A97, A94
.= F2 ;
A104: t19 = [[F19,F29],t19] `2
.= [[F1,F2],t] `2 by A97, A94
.= t ;
A105: t19 `*` (id F19) = t19 by Th20, A102;
cod ii = ([[F,F],(id F)] `1) `2 by A89, A26
.= a by A88 ;
then [f,ii] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A41, A93;
hence f (*) ii = m . (f,ii) by CAT_1:def 1
.= f by A104, A105, A95, A103, A96, A91, A100, A101, A98, A89, A94, XTUPLE_0:1 ;
:: thesis: verum

end;

assume A106: Hom (b,a) <> {} ; :: thesis: for f being Morphism of b,a holds ii (*) f = f
let f be Morphism of b,a; :: thesis: ii (*) f = f
reconsider f9 = f as Element of NatTrans (A,B) ;
A107: cod f = a by A106, CAT_1:5;
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A108: f9 = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def15;
A109: F2 = [F1,F2] `2
.= (f9 `1) `2 by A108
.= cod f by A26
.= F by A106, A88, CAT_1:5 ;
then reconsider t = t as natural_transformation of F1,F ;
S<sub>1</sub>[s,f9,[[F1,F],((id F) `*` t)]] by A108, A109;
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
A110: f9 = [[F9,F19],t9] and
A111: i . F = [[F19,F29],t19] and
A112: m . ((i . F),f9) = [[F9,F29],(t19 `*` t9)] by A20, A91, A19;
A113: t19 = id F by A111, A91, XTUPLE_0:1;
A114: [F19,F29] = [F,F] by A111, A91, XTUPLE_0:1;
then A115: F19 = F by XTUPLE_0:1;
A116: F9 is_naturally_transformable_to F19 by A110, Th28;
A117: F9 = ([[F9,F19],t9] `1) `1
.= ([[F1,F2],t] `1) `1 by A110, A108
.= F1 ;
A118: t9 = [[F9,F19],t9] `2
.= [[F1,F2],t] `2 by A110, A108
.= t ;
A119: (id F19) `*` t9 = t9 by Th20, A116;
dom ii = ([[F,F],(id F)] `1) `1 by A89, A23
.= a by A88 ;
then [ii,f] in dom the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) by A41, A107;
hence ii (*) f = m . (ii,f) by CAT_1:def 1
.= m . ((i . F),f9) by A89, A90, A28
.= [[F9,F29],((id F19) `*` t9)] by A113, A115, A114, A112, XTUPLE_0:1
.= f by A108, A118, A119, A114, A109, A117, XTUPLE_0:1 ;
:: thesis: verum

end;

CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is with_identities

proof

let a be Element of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def 10 :: thesis: ex b₁ being Morphism of a,a st
for b₂ being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b₂) = {} or for b₃ being Morphism of a,b₂ holds b₃ (*) b₁ = b₃ ) & ( Hom (b₂,a) = {} or for b₃ being Morphism of b₂,a holds b₁ (*) b₃ = b₃ ) )
reconsider F = a as Functor of A,B by CAT_2:def 2;
reconsider s = [[F,F],(id F)] as Element of NatTrans (A,B) by Def15;
reconsider s = s as Morphism of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) ;
A120: dom s = ([[F,F],(id F)] `1) `1 by A23
.= F ;
cod s = ([[F,F],(id F)] `1) `2 by A26
.= F ;
then s in Hom (a,a) by A120;
then reconsider s = s as Morphism of a,a by CAT_1:def 5;
take s ; :: thesis: for b₁ being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b₁) = {} or for b₂ being Morphism of a,b₁ holds b₂ (*) s = b₂ ) & ( Hom (b₁,a) = {} or for b₂ being Morphism of b₁,a holds s (*) b₂ = b₂ ) )
thus for b₁ being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds
( ( Hom (a,b₁) = {} or for b₂ being Morphism of a,b₁ holds b₂ (*) s = b₂ ) & ( Hom (b₁,a) = {} or for b₂ being Morphism of b₁,a holds s (*) b₂ = b₂ ) ) by A87; :: thesis: verum

end;

then reconsider C = CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) as strict Category by A41, A50, A65, A85;
take C ; :: thesis: ( the carrier of C = Funct (A,B) & the carrier' of C = NatTrans (A,B) & ( for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( 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)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus ( the carrier of C = Funct (A,B) & the carrier' of C = NatTrans (A,B) ) ; :: thesis: ( ( for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) ) & ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( 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)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus for f being Morphism of C holds
( dom f = (f `1) `1 & cod f = (f `1) `2 ) by A23, A26; :: thesis: ( ( for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C ) & ( 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)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )
thus for f, g being Morphism of C st dom g = cod f holds
[g,f] in dom the Comp of C :: thesis: ( ( 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)] ) ) & ( for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)] ) )

proof

let f, g be Morphism of C; :: thesis: ( dom g = cod f implies [g,f] in dom the Comp of C )
assume A121: dom g = cod f ; :: thesis: [g,f] in dom the Comp of C
consider F19, F29 being Functor of A,B, t9 being natural_transformation of F19,F29 such that
A122: g = [[F19,F29],t9] and
F19 is_naturally_transformable_to F29 by Def15;
consider F1, F2 being Functor of A,B, t being natural_transformation of F1,F2 such that
A123: f = [[F1,F2],t] and
F1 is_naturally_transformable_to F2 by Def15;
A124: F2 = ([[F1,F2],t] `1) `2
.= cod f by A26, A123
.= ([[F19,F29],t9] `1) `1 by A23, A122, A121
.= F19 ;
then reconsider t9 = t9 as natural_transformation of F2,F29 ;
S₁[g,f,[[F1,F29],(t9 `*` t)]] by A123, A122, A124;
hence [g,f] in dom the Comp of C by A19; :: thesis: verum

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: for a being Object of C
for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]

proof

let f, g be Morphism of C; :: thesis: ( [g,f] in dom the Comp of C implies 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)] ) )
assume [g,f] in dom the Comp of C ; :: thesis: 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)] )
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: verum

end;

let a be Object of C; :: thesis: for F being Functor of A,B st F = a holds
id a = [[F,F],(id F)]
let F be Functor of A,B; :: thesis: ( F = a implies id a = [[F,F],(id F)] )
assume A125: a = F ; :: thesis: id a = [[F,F],(id F)]
reconsider m = [[F,F],(id F)] as Element of NatTrans (A,B) by Def15;
reconsider m = m as Morphism of C ;
A126: dom m = ([[F,F],(id F)] `1) `1 by A23
.= F ;
cod m = ([[F,F],(id F)] `1) `2 by A26
.= F ;
then m in Hom (a,a) by A125, A126;
then reconsider m = m as Morphism of a,a by CAT_1:def 5;
for b being Object of C holds
( ( Hom (a,b) <> {} implies for f being Morphism of a,b holds f (*) m = f ) & ( Hom (b,a) <> {} implies for f being Morphism of b,a holds m (*) f = f ) ) by A125, A87;
hence id a = [[F,F],(id F)] by CAT_1:def 12; :: thesis: verum