defpred S_{1}[ 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_{1}( object ) -> object = ($1 `1) `1 ;

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_{1}[x,y,z] ) )
and

A20: for x, y being object st [x,y] in dom m holds

S_{1}[x,y,m . (x,y)]
from BINOP_1:sch 5(A12, A1);

A23: for t being Element of NatTrans (A,B) holds d . t = H_{1}(t)
from FUNCT_2:sch 8(A21);

deffunc H_{2}( set ) -> object = ($1 `1) `2 ;

A26: for t being Element of NatTrans (A,B) holds c . t = H_{2}(t)
from FUNCT_2:sch 8(A24);

deffunc H_{3}( Element of Funct (A,B)) -> object = [[$1,$1],(id $1)];

A27: for F being Element of Funct (A,B) holds H_{3}(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_{3}(F)
from FUNCT_2:sch 8(A27);

set C = 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 ) )

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)] ) )

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)]

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

( $2 = [[F,F1],t] & $1 = [[F1,F2],t1] & $3 = [[F,F2],(t1 `*` t)] );

deffunc H

A1: now :: thesis: for x, y, z1, z2 being object st x in NatTrans (A,B) & y in NatTrans (A,B) & S_{1}[x,y,z1] & S_{1}[x,y,z2] holds

z1 = z2

z1 = z2

let x, y, z1, z2 be object ; :: thesis: ( x in NatTrans (A,B) & y in NatTrans (A,B) & S_{1}[x,y,z1] & S_{1}[x,y,z2] implies z1 = z2 )

assume that

x in NatTrans (A,B) and

y in NatTrans (A,B) ; :: thesis: ( S_{1}[x,y,z1] & S_{1}[x,y,z2] implies z1 = z2 )

assume S_{1}[x,y,z1]
; :: thesis: ( S_{1}[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_{1}[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;assume that

x in NatTrans (A,B) and

y in NatTrans (A,B) ; :: thesis: ( S

assume S

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

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

A12: now :: thesis: for x, y, z being object st x in NatTrans (A,B) & y in NatTrans (A,B) & S_{1}[x,y,z] holds

z in NatTrans (A,B)

consider m being PartFunc of [:(NatTrans (A,B)),(NatTrans (A,B)):],(NatTrans (A,B)) such that z in NatTrans (A,B)

let x, y, z be object ; :: thesis: ( x in NatTrans (A,B) & y in NatTrans (A,B) & S_{1}[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_{1}[x,y,z] implies z in NatTrans (A,B) )

assume S_{1}[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;assume that

A13: x in NatTrans (A,B) and

A14: y in NatTrans (A,B) ; :: thesis: ( S

assume S

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

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

A20: for x, y being object st [x,y] in dom m holds

S

A21: now :: thesis: for t being Element of NatTrans (A,B) holds H_{1}(t) in Funct (A,B)

consider d being Function of (NatTrans (A,B)),(Funct (A,B)) such that let t be Element of NatTrans (A,B); :: thesis: H_{1}(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_{1}(t) in Funct (A,B)
by CAT_2:def 2; :: thesis: verum

end;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

A23: for t being Element of NatTrans (A,B) holds d . t = H

deffunc H

A24: now :: thesis: for t being Element of NatTrans (A,B) holds H_{2}(t) in Funct (A,B)

consider c being Function of (NatTrans (A,B)),(Funct (A,B)) such that let t be Element of NatTrans (A,B); :: thesis: H_{2}(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_{2}(t) in Funct (A,B)
by CAT_2:def 2; :: thesis: verum

end;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

A26: for t being Element of NatTrans (A,B) holds c . t = H

deffunc H

A27: for F being Element of Funct (A,B) holds H

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

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)]

A41:
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is Category-like
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_{1}[[[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;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] 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

proof

A50:
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is transitive
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 #) )

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;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 A46:
dom g = cod f
; :: thesis: [g,f] in proj1 the Comp of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #)
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;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

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

proof

A65:
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is associative
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;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

proof

A85:
CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is reflexive
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;( [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

proof

A87:
for a being Object of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #)
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;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

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

CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) is with_identities
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 )

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_{1}[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;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 A106:
Hom (b,a) <> {}
; :: thesis: for f being Morphism of b,a holds ii (*) f = f
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_{1}[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;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

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

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

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

proof

then reconsider C = CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) as strict Category by A41, A50, A65, A85;
let a be Element of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #); :: according to CAT_1:def 10 :: thesis: ex b_{1} being Morphism of a,a st

for b_{2} being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds

( ( Hom (a,b_{2}) = {} or for b_{3} being Morphism of a,b_{2} holds b_{3} (*) b_{1} = b_{3} ) & ( Hom (b_{2},a) = {} or for b_{3} being Morphism of b_{2},a holds b_{1} (*) b_{3} = b_{3} ) )

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_{1} being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds

( ( Hom (a,b_{1}) = {} or for b_{2} being Morphism of a,b_{1} holds b_{2} (*) s = b_{2} ) & ( Hom (b_{1},a) = {} or for b_{2} being Morphism of b_{1},a holds s (*) b_{2} = b_{2} ) )

thus for b_{1} being Element of the carrier of CatStr(# (Funct (A,B)),(NatTrans (A,B)),d,c,m #) holds

( ( Hom (a,b_{1}) = {} or for b_{2} being Morphism of a,b_{1} holds b_{2} (*) s = b_{2} ) & ( Hom (b_{1},a) = {} or for b_{2} being Morphism of b_{1},a holds s (*) b_{2} = b_{2} ) )
by A87; :: thesis: verum

end;for b

( ( Hom (a,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

( ( Hom (a,b

thus for b

( ( Hom (a,b

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

thus
for f, g being Morphism of C st [g,f] in dom the Comp of C holds
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_{1}[g,f,[[F1,F29],(t9 `*` t)]]
by A123, A122, A124;

hence [g,f] in dom the Comp of C by A19; :: thesis: verum

end;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

hence [g,f] in dom the Comp of C by A19; :: thesis: verum

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 a be Object of C; :: thesis: for F being Functor of A,B st F = a holds
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;( 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

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