defpred S_{1}[ object , object , object ] means for f, g, h being strict covariant Functor of A,B st [f,g,h] = $3 holds

for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h st [t2,t1] = $2 & ex v being Function st v . $2 = $1 holds

$1 = t2 `*` t1;

defpred S_{2}[ object , object ] means ex D2 being set st

( D2 = $2 & ( for f, g being strict covariant Functor of A,B st [f,g] = $1 holds

for x being set holds

( x in D2 iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) ) );

A1: for i being object st i in [:(Funct (A,B)),(Funct (A,B)):] holds

ex j being object st S_{2}[i,j]

A17: for i being object st i in [:(Funct (A,B)),(Funct (A,B)):] holds

S_{2}[i,a . i]
from PBOOLE:sch 3(A1);

A18: for o being object st o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] holds

for x being object st x in {|a,a|} . o holds

ex y being object st

( y in {|a|} . o & S_{1}[y,x,o] )

A40: for i being object st i in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] holds

ex v being Function of ({|a,a|} . i),({|a|} . i) st

( v = c . i & ( for x being object st x in {|a,a|} . i holds

S_{1}[v . x,x,i] ) )
from MSSUBFAM:sch 1(A18);

set F = AltCatStr(# (Funct (A,B)),a,c #);

A41: not Funct (A,B) is empty

take F ; :: thesis: ( the carrier of F = Funct (A,B) & ( for F, G being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of F . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds

for t1 being natural_transformation of F,G

for t2 being natural_transformation of G,H ex f being Function st

( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) )

thus the carrier of F = Funct (A,B) ; :: thesis: ( ( for F, G being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of F . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds

for t1 being natural_transformation of F,G

for t2 being natural_transformation of G,H ex f being Function st

( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) )

thus for f, g being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) :: thesis: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds

for t1 being natural_transformation of F,G

for t2 being natural_transformation of G,H ex f being Function st

( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 )

for t2 being natural_transformation of g,h ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) )

assume that

A55: f is_naturally_transformable_to g and

A56: g is_naturally_transformable_to h ; :: thesis: for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )

let t1 be natural_transformation of f,g; :: thesis: for t2 being natural_transformation of g,h ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )

let t2 be natural_transformation of g,h; :: thesis: ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )

A57: f in Funct (A,B) by Def10;

then reconsider T = Funct (A,B) as non empty set ;

A58: g in Funct (A,B) by Def10;

then A59: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by A57, ZFMISC_1:87;

A60: h in Funct (A,B) by Def10;

then [g,h] in [:(Funct (A,B)),(Funct (A,B)):] by A58, ZFMISC_1:87;

then S_{2}[[g,h],a . [g,h]]
by A17;

then A61: t2 in a . [g,h] by A56;

reconsider i = f, j = g, k = h as Element of T by Def10;

A62: {|a,a|} . [i,j,k] = {|a,a|} . (i,j,k) by MULTOP_1:def 1

.= [:(a . (j,k)),(a . (i,j)):] by ALTCAT_1:def 4 ;

( [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] = [:[:(Funct (A,B)),(Funct (A,B)):],(Funct (A,B)):] & [f,g,h] = [[f,g],h] ) by ZFMISC_1:def 3;

then [f,g,h] in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] by A60, A59, ZFMISC_1:87;

then consider v being Function of ({|a,a|} . [f,g,h]),({|a|} . [f,g,h]) such that

A63: v = c . [f,g,h] and

A64: for x being object st x in {|a,a|} . [f,g,h] holds

S_{1}[v . x,x,[f,g,h]]
by A40;

S_{2}[[f,g],a . [f,g]]
by A17, A59;

then t1 in a . [f,g] by A55;

then [t2,t1] in {|a,a|} . [f,g,h] by A62, A61, ZFMISC_1:87;

then A65: v . (t2,t1) = t2 `*` t1 by A64;

v = c . (f,g,h) by A63, MULTOP_1:def 1;

hence ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) by A65; :: thesis: verum

for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h st [t2,t1] = $2 & ex v being Function st v . $2 = $1 holds

$1 = t2 `*` t1;

defpred S

( D2 = $2 & ( for f, g being strict covariant Functor of A,B st [f,g] = $1 holds

for x being set holds

( x in D2 iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) ) );

A1: for i being object st i in [:(Funct (A,B)),(Funct (A,B)):] holds

ex j being object st S

proof

consider a being ManySortedSet of [:(Funct (A,B)),(Funct (A,B)):] such that
let i be object ; :: thesis: ( i in [:(Funct (A,B)),(Funct (A,B)):] implies ex j being object st S_{2}[i,j] )

assume i in [:(Funct (A,B)),(Funct (A,B)):] ; :: thesis: ex j being object st S_{2}[i,j]

then consider f, g being object such that

A2: ( f in Funct (A,B) & g in Funct (A,B) ) and

A3: i = [f,g] by ZFMISC_1:def 2;

reconsider f = f, g = g as strict covariant Functor of A,B by A2, Def10;

defpred S_{3}[ Object of A, object ] means $2 = <^(f . $1),(g . $1)^>;

defpred S_{4}[ object ] means ( f is_naturally_transformable_to g & $1 is natural_transformation of f,g );

A4: for a being Element of A ex j being object st S_{3}[a,j]
;

consider N being ManySortedSet of the carrier of A such that

A5: for a being Element of A holds S_{3}[a,N . a]
from PBOOLE:sch 6(A4);

consider j being set such that

A6: for x being object holds

( x in j iff ( x in product N & S_{4}[x] ) )
from XBOOLE_0:sch 1();

take j ; :: thesis: S_{2}[i,j]

take j ; :: thesis: ( j = j & ( for f, g being strict covariant Functor of A,B st [f,g] = i holds

for x being set holds

( x in j iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) ) )

thus j = j ; :: thesis: for f, g being strict covariant Functor of A,B st [f,g] = i holds

for x being set holds

( x in j iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) )

let f9, g9 be strict covariant Functor of A,B; :: thesis: ( [f9,g9] = i implies for x being set holds

( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) )

assume A7: [f9,g9] = i ; :: thesis: for x being set holds

( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) )

let x be set ; :: thesis: ( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) )

thus ( x in j implies ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) :: thesis: ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 implies x in j )

end;assume i in [:(Funct (A,B)),(Funct (A,B)):] ; :: thesis: ex j being object st S

then consider f, g being object such that

A2: ( f in Funct (A,B) & g in Funct (A,B) ) and

A3: i = [f,g] by ZFMISC_1:def 2;

reconsider f = f, g = g as strict covariant Functor of A,B by A2, Def10;

defpred S

defpred S

A4: for a being Element of A ex j being object st S

consider N being ManySortedSet of the carrier of A such that

A5: for a being Element of A holds S

consider j being set such that

A6: for x being object holds

( x in j iff ( x in product N & S

take j ; :: thesis: S

take j ; :: thesis: ( j = j & ( for f, g being strict covariant Functor of A,B st [f,g] = i holds

for x being set holds

( x in j iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) ) )

thus j = j ; :: thesis: for f, g being strict covariant Functor of A,B st [f,g] = i holds

for x being set holds

( x in j iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) )

let f9, g9 be strict covariant Functor of A,B; :: thesis: ( [f9,g9] = i implies for x being set holds

( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) )

assume A7: [f9,g9] = i ; :: thesis: for x being set holds

( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) )

let x be set ; :: thesis: ( x in j iff ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) )

thus ( x in j implies ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) ) :: thesis: ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 implies x in j )

proof

thus
( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 implies x in j )
:: thesis: verum
assume A8:
x in j
; :: thesis: ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 )

( f9 = f & g9 = g ) by A3, A7, XTUPLE_0:1;

hence ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) by A6, A8; :: thesis: verum

end;( f9 = f & g9 = g ) by A3, A7, XTUPLE_0:1;

hence ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 ) by A6, A8; :: thesis: verum

proof

A9:
( f9 = f & g9 = g )
by A3, A7, XTUPLE_0:1;

set I = the carrier of A;

assume that

A10: f9 is_naturally_transformable_to g9 and

A11: x is natural_transformation of f9,g9 ; :: thesis: x in j

reconsider h = x as ManySortedSet of the carrier of A by A11;

A12: f9 is_transformable_to g9 by A10;

A13: for i9 being set st i9 in the carrier of A holds

h . i9 in N . i9

h . i9 in N . i9

then dom h = dom N by PARTFUN1:def 2;

then x in product N by A15, CARD_3:9;

hence x in j by A6, A10, A11, A9; :: thesis: verum

end;set I = the carrier of A;

assume that

A10: f9 is_naturally_transformable_to g9 and

A11: x is natural_transformation of f9,g9 ; :: thesis: x in j

reconsider h = x as ManySortedSet of the carrier of A by A11;

A12: f9 is_transformable_to g9 by A10;

A13: for i9 being set st i9 in the carrier of A holds

h . i9 in N . i9

proof

A15:
for i9 being object st i9 in dom N holds
let i9 be set ; :: thesis: ( i9 in the carrier of A implies h . i9 in N . i9 )

assume i9 in the carrier of A ; :: thesis: h . i9 in N . i9

then reconsider i9 = i9 as Element of A ;

A14: S_{3}[i9,N . i9]
by A5;

( <^(f . i9),(g . i9)^> <> {} & h . i9 is Element of <^(f . i9),(g . i9)^> ) by A11, A12, A9, Def2;

hence h . i9 in N . i9 by A14; :: thesis: verum

end;assume i9 in the carrier of A ; :: thesis: h . i9 in N . i9

then reconsider i9 = i9 as Element of A ;

A14: S

( <^(f . i9),(g . i9)^> <> {} & h . i9 is Element of <^(f . i9),(g . i9)^> ) by A11, A12, A9, Def2;

hence h . i9 in N . i9 by A14; :: thesis: verum

h . i9 in N . i9

proof

dom h = the carrier of A
by PARTFUN1:def 2;
A16:
dom N = the carrier of A
by PARTFUN1:def 2;

let i9 be object ; :: thesis: ( i9 in dom N implies h . i9 in N . i9 )

assume i9 in dom N ; :: thesis: h . i9 in N . i9

hence h . i9 in N . i9 by A13, A16; :: thesis: verum

end;let i9 be object ; :: thesis: ( i9 in dom N implies h . i9 in N . i9 )

assume i9 in dom N ; :: thesis: h . i9 in N . i9

hence h . i9 in N . i9 by A13, A16; :: thesis: verum

then dom h = dom N by PARTFUN1:def 2;

then x in product N by A15, CARD_3:9;

hence x in j by A6, A10, A11, A9; :: thesis: verum

A17: for i being object st i in [:(Funct (A,B)),(Funct (A,B)):] holds

S

A18: for o being object st o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] holds

for x being object st x in {|a,a|} . o holds

ex y being object st

( y in {|a|} . o & S

proof

consider c being ManySortedFunction of {|a,a|},{|a|} such that
let o be object ; :: thesis: ( o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] implies for x being object st x in {|a,a|} . o holds

ex y being object st

( y in {|a|} . o & S_{1}[y,x,o] ) )

assume o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] ; :: thesis: for x being object st x in {|a,a|} . o holds

ex y being object st

( y in {|a|} . o & S_{1}[y,x,o] )

then o in [:[:(Funct (A,B)),(Funct (A,B)):],(Funct (A,B)):] by ZFMISC_1:def 3;

then consider ff, h being object such that

A19: ff in [:(Funct (A,B)),(Funct (A,B)):] and

A20: h in Funct (A,B) and

A21: o = [ff,h] by ZFMISC_1:def 2;

consider f, g being object such that

A22: ( f in Funct (A,B) & g in Funct (A,B) ) and

A23: ff = [f,g] by A19, ZFMISC_1:def 2;

A24: o = [f,g,h] by A21, A23;

reconsider T = Funct (A,B) as non empty set by A20;

reconsider i = f, j = g, k = h as Element of T by A20, A22;

A25: {|a|} . [i,j,k] = {|a|} . (i,j,k) by MULTOP_1:def 1

.= a . (i,k) by ALTCAT_1:def 3 ;

A26: {|a,a|} . [i,j,k] = {|a,a|} . (i,j,k) by MULTOP_1:def 1

.= [:(a . (j,k)),(a . (i,j)):] by ALTCAT_1:def 4 ;

for x being object st x in {|a,a|} . o holds

ex y being object st

( y in {|a|} . o & S_{1}[y,x,o] )

ex y being object st

( y in {|a|} . o & S_{1}[y,x,o] )
; :: thesis: verum

end;ex y being object st

( y in {|a|} . o & S

assume o in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] ; :: thesis: for x being object st x in {|a,a|} . o holds

ex y being object st

( y in {|a|} . o & S

then o in [:[:(Funct (A,B)),(Funct (A,B)):],(Funct (A,B)):] by ZFMISC_1:def 3;

then consider ff, h being object such that

A19: ff in [:(Funct (A,B)),(Funct (A,B)):] and

A20: h in Funct (A,B) and

A21: o = [ff,h] by ZFMISC_1:def 2;

consider f, g being object such that

A22: ( f in Funct (A,B) & g in Funct (A,B) ) and

A23: ff = [f,g] by A19, ZFMISC_1:def 2;

A24: o = [f,g,h] by A21, A23;

reconsider T = Funct (A,B) as non empty set by A20;

reconsider i = f, j = g, k = h as Element of T by A20, A22;

A25: {|a|} . [i,j,k] = {|a|} . (i,j,k) by MULTOP_1:def 1

.= a . (i,k) by ALTCAT_1:def 3 ;

A26: {|a,a|} . [i,j,k] = {|a,a|} . (i,j,k) by MULTOP_1:def 1

.= [:(a . (j,k)),(a . (i,j)):] by ALTCAT_1:def 4 ;

for x being object st x in {|a,a|} . o holds

ex y being object st

( y in {|a|} . o & S

proof

hence
for x being object st x in {|a,a|} . o holds
reconsider i9 = i, j9 = j, k9 = k as strict covariant Functor of A,B by Def10;

let x be object ; :: thesis: ( x in {|a,a|} . o implies ex y being object st

( y in {|a|} . o & S_{1}[y,x,o] ) )

assume x in {|a,a|} . o ; :: thesis: ex y being object st

( y in {|a|} . o & S_{1}[y,x,o] )

then consider x2, x1 being object such that

A27: x2 in a . (j,k) and

A28: x1 in a . (i,j) and

A29: x = [x2,x1] by A24, A26, ZFMISC_1:def 2;

A30: x2 in a . [j,k] by A27;

A31: S_{2}[[j,k],a . [j,k]]
by A17;

then A32: j9 is_naturally_transformable_to k9 by A30;

reconsider x2 = x2 as natural_transformation of j9,k9 by A30, A31;

A33: x1 in a . [i,j] by A28;

S_{2}[[i,j],a . [i,j]]
by A17;

then reconsider x1 = x1 as natural_transformation of i9,j9 by A33;

reconsider vv = x2 `*` x1 as natural_transformation of i9,k9 ;

A34: for f, g, h being strict covariant Functor of A,B st [f,g,h] = o holds

for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds

vv = t2 `*` t1_{2}[[i,j],a . [i,j]]
by A17;

then i9 is_naturally_transformable_to j9 by A33;

then A39: i9 is_naturally_transformable_to k9 by A32, Th8;

S_{2}[[i,k],a . [i,k]]
by A17;

then vv in a . [i9,k9] by A39;

hence ex y being object st

( y in {|a|} . o & S_{1}[y,x,o] )
by A24, A25, A34; :: thesis: verum

end;let x be object ; :: thesis: ( x in {|a,a|} . o implies ex y being object st

( y in {|a|} . o & S

assume x in {|a,a|} . o ; :: thesis: ex y being object st

( y in {|a|} . o & S

then consider x2, x1 being object such that

A27: x2 in a . (j,k) and

A28: x1 in a . (i,j) and

A29: x = [x2,x1] by A24, A26, ZFMISC_1:def 2;

A30: x2 in a . [j,k] by A27;

A31: S

then A32: j9 is_naturally_transformable_to k9 by A30;

reconsider x2 = x2 as natural_transformation of j9,k9 by A30, A31;

A33: x1 in a . [i,j] by A28;

S

then reconsider x1 = x1 as natural_transformation of i9,j9 by A33;

reconsider vv = x2 `*` x1 as natural_transformation of i9,k9 ;

A34: for f, g, h being strict covariant Functor of A,B st [f,g,h] = o holds

for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds

vv = t2 `*` t1

proof

S
let f, g, h be strict covariant Functor of A,B; :: thesis: ( [f,g,h] = o implies for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds

vv = t2 `*` t1 )

assume A35: [f,g,h] = o ; :: thesis: for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds

vv = t2 `*` t1

A36: j9 = g by A24, A35, XTUPLE_0:3;

then reconsider x2 = x2 as natural_transformation of g,h by A24, A35, XTUPLE_0:3;

A37: ( i9 = f & k9 = h ) by A24, A35, XTUPLE_0:3;

let t1 be natural_transformation of f,g; :: thesis: for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds

vv = t2 `*` t1

let t2 be natural_transformation of g,h; :: thesis: ( [t2,t1] = x & ex v being Function st v . x = vv implies vv = t2 `*` t1 )

assume that

A38: [t2,t1] = x and

ex v being Function st v . x = vv ; :: thesis: vv = t2 `*` t1

x2 = t2 by A29, A38, XTUPLE_0:1;

hence vv = t2 `*` t1 by A29, A38, A36, A37, XTUPLE_0:1; :: thesis: verum

end;for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds

vv = t2 `*` t1 )

assume A35: [f,g,h] = o ; :: thesis: for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds

vv = t2 `*` t1

A36: j9 = g by A24, A35, XTUPLE_0:3;

then reconsider x2 = x2 as natural_transformation of g,h by A24, A35, XTUPLE_0:3;

A37: ( i9 = f & k9 = h ) by A24, A35, XTUPLE_0:3;

let t1 be natural_transformation of f,g; :: thesis: for t2 being natural_transformation of g,h st [t2,t1] = x & ex v being Function st v . x = vv holds

vv = t2 `*` t1

let t2 be natural_transformation of g,h; :: thesis: ( [t2,t1] = x & ex v being Function st v . x = vv implies vv = t2 `*` t1 )

assume that

A38: [t2,t1] = x and

ex v being Function st v . x = vv ; :: thesis: vv = t2 `*` t1

x2 = t2 by A29, A38, XTUPLE_0:1;

hence vv = t2 `*` t1 by A29, A38, A36, A37, XTUPLE_0:1; :: thesis: verum

then i9 is_naturally_transformable_to j9 by A33;

then A39: i9 is_naturally_transformable_to k9 by A32, Th8;

S

then vv in a . [i9,k9] by A39;

hence ex y being object st

( y in {|a|} . o & S

ex y being object st

( y in {|a|} . o & S

A40: for i being object st i in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] holds

ex v being Function of ({|a,a|} . i),({|a|} . i) st

( v = c . i & ( for x being object st x in {|a,a|} . i holds

S

set F = AltCatStr(# (Funct (A,B)),a,c #);

A41: not Funct (A,B) is empty

proof

AltCatStr(# (Funct (A,B)),a,c #) is transitive
set f = the strict covariant Functor of A,B;

the strict covariant Functor of A,B in Funct (A,B) by Def10;

hence not Funct (A,B) is empty ; :: thesis: verum

end;the strict covariant Functor of A,B in Funct (A,B) by Def10;

hence not Funct (A,B) is empty ; :: thesis: verum

proof

then reconsider F = AltCatStr(# (Funct (A,B)),a,c #) as non empty transitive strict AltCatStr by A41;
let o1, o2, o3 be Object of AltCatStr(# (Funct (A,B)),a,c #); :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )

reconsider a1 = o1, a2 = o2, a3 = o3 as strict covariant Functor of A,B by A41, Def10;

assume that

A42: <^o1,o2^> <> {} and

A43: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}

consider x being object such that

A44: x in a . [o2,o3] by A43, XBOOLE_0:def 1;

[o2,o3] in [:(Funct (A,B)),(Funct (A,B)):] by A41, ZFMISC_1:def 2;

then A45: S_{2}[[o2,o3],a . [o2,o3]]
by A17;

then A46: a2 is_naturally_transformable_to a3 by A44;

reconsider x = x as natural_transformation of a2,a3 by A44, A45;

consider y being object such that

A47: y in a . [o1,o2] by A42, XBOOLE_0:def 1;

[o1,o2] in [:(Funct (A,B)),(Funct (A,B)):] by A41, ZFMISC_1:def 2;

then A48: S_{2}[[o1,o2],a . [o1,o2]]
by A17;

then reconsider y = y as natural_transformation of a1,a2 by A47;

a1 is_naturally_transformable_to a2 by A47, A48;

then A49: a1 is_naturally_transformable_to a3 by A46, Th8;

A50: ( x `*` y is natural_transformation of a1,a3 & [o1,o3] in [:(Funct (A,B)),(Funct (A,B)):] ) by A41, ZFMISC_1:def 2;

then S_{2}[[o1,o3],a . [o1,o3]]
by A17;

hence not <^o1,o3^> = {} by A49, A50; :: thesis: verum

end;reconsider a1 = o1, a2 = o2, a3 = o3 as strict covariant Functor of A,B by A41, Def10;

assume that

A42: <^o1,o2^> <> {} and

A43: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}

consider x being object such that

A44: x in a . [o2,o3] by A43, XBOOLE_0:def 1;

[o2,o3] in [:(Funct (A,B)),(Funct (A,B)):] by A41, ZFMISC_1:def 2;

then A45: S

then A46: a2 is_naturally_transformable_to a3 by A44;

reconsider x = x as natural_transformation of a2,a3 by A44, A45;

consider y being object such that

A47: y in a . [o1,o2] by A42, XBOOLE_0:def 1;

[o1,o2] in [:(Funct (A,B)),(Funct (A,B)):] by A41, ZFMISC_1:def 2;

then A48: S

then reconsider y = y as natural_transformation of a1,a2 by A47;

a1 is_naturally_transformable_to a2 by A47, A48;

then A49: a1 is_naturally_transformable_to a3 by A46, Th8;

A50: ( x `*` y is natural_transformation of a1,a3 & [o1,o3] in [:(Funct (A,B)),(Funct (A,B)):] ) by A41, ZFMISC_1:def 2;

then S

hence not <^o1,o3^> = {} by A49, A50; :: thesis: verum

take F ; :: thesis: ( the carrier of F = Funct (A,B) & ( for F, G being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of F . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds

for t1 being natural_transformation of F,G

for t2 being natural_transformation of G,H ex f being Function st

( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) )

thus the carrier of F = Funct (A,B) ; :: thesis: ( ( for F, G being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of F . (F,G) iff ( F is_naturally_transformable_to G & x is natural_transformation of F,G ) ) ) & ( for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds

for t1 being natural_transformation of F,G

for t2 being natural_transformation of G,H ex f being Function st

( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 ) ) )

thus for f, g being strict covariant Functor of A,B

for x being set holds

( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) :: thesis: for F, G, H being strict covariant Functor of A,B st F is_naturally_transformable_to G & G is_naturally_transformable_to H holds

for t1 being natural_transformation of F,G

for t2 being natural_transformation of G,H ex f being Function st

( f = the Comp of F . (F,G,H) & f . (t2,t1) = t2 `*` t1 )

proof

let f, g, h be strict covariant Functor of A,B; :: thesis: ( f is_naturally_transformable_to g & g is_naturally_transformable_to h implies for t1 being natural_transformation of f,g
let f, g be strict covariant Functor of A,B; :: thesis: for x being set holds

( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) )

let x be set ; :: thesis: ( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) )

thus ( x in the Arrows of F . (f,g) implies ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) :: thesis: ( f is_naturally_transformable_to g & x is natural_transformation of f,g implies x in the Arrows of F . (f,g) )

end;( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) )

let x be set ; :: thesis: ( x in the Arrows of F . (f,g) iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) )

thus ( x in the Arrows of F . (f,g) implies ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) :: thesis: ( f is_naturally_transformable_to g & x is natural_transformation of f,g implies x in the Arrows of F . (f,g) )

proof

thus
( f is_naturally_transformable_to g & x is natural_transformation of f,g implies x in the Arrows of F . (f,g) )
:: thesis: verum
( f in Funct (A,B) & g in Funct (A,B) )
by Def10;

then A51: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:def 2;

assume A52: x in the Arrows of F . (f,g) ; :: thesis: ( f is_naturally_transformable_to g & x is natural_transformation of f,g )

S_{2}[[f,g],a . [f,g]]
by A17, A51;

hence ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) by A52; :: thesis: verum

end;then A51: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:def 2;

assume A52: x in the Arrows of F . (f,g) ; :: thesis: ( f is_naturally_transformable_to g & x is natural_transformation of f,g )

S

hence ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) by A52; :: thesis: verum

proof

( f in Funct (A,B) & g in Funct (A,B) )
by Def10;

then A53: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:87;

assume A54: ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ; :: thesis: x in the Arrows of F . (f,g)

S_{2}[[f,g],a . [f,g]]
by A17, A53;

hence x in the Arrows of F . (f,g) by A54; :: thesis: verum

end;then A53: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by ZFMISC_1:87;

assume A54: ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ; :: thesis: x in the Arrows of F . (f,g)

S

hence x in the Arrows of F . (f,g) by A54; :: thesis: verum

for t2 being natural_transformation of g,h ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) )

assume that

A55: f is_naturally_transformable_to g and

A56: g is_naturally_transformable_to h ; :: thesis: for t1 being natural_transformation of f,g

for t2 being natural_transformation of g,h ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )

let t1 be natural_transformation of f,g; :: thesis: for t2 being natural_transformation of g,h ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )

let t2 be natural_transformation of g,h; :: thesis: ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 )

A57: f in Funct (A,B) by Def10;

then reconsider T = Funct (A,B) as non empty set ;

A58: g in Funct (A,B) by Def10;

then A59: [f,g] in [:(Funct (A,B)),(Funct (A,B)):] by A57, ZFMISC_1:87;

A60: h in Funct (A,B) by Def10;

then [g,h] in [:(Funct (A,B)),(Funct (A,B)):] by A58, ZFMISC_1:87;

then S

then A61: t2 in a . [g,h] by A56;

reconsider i = f, j = g, k = h as Element of T by Def10;

A62: {|a,a|} . [i,j,k] = {|a,a|} . (i,j,k) by MULTOP_1:def 1

.= [:(a . (j,k)),(a . (i,j)):] by ALTCAT_1:def 4 ;

( [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] = [:[:(Funct (A,B)),(Funct (A,B)):],(Funct (A,B)):] & [f,g,h] = [[f,g],h] ) by ZFMISC_1:def 3;

then [f,g,h] in [:(Funct (A,B)),(Funct (A,B)),(Funct (A,B)):] by A60, A59, ZFMISC_1:87;

then consider v being Function of ({|a,a|} . [f,g,h]),({|a|} . [f,g,h]) such that

A63: v = c . [f,g,h] and

A64: for x being object st x in {|a,a|} . [f,g,h] holds

S

S

then t1 in a . [f,g] by A55;

then [t2,t1] in {|a,a|} . [f,g,h] by A62, A61, ZFMISC_1:87;

then A65: v . (t2,t1) = t2 `*` t1 by A64;

v = c . (f,g,h) by A63, MULTOP_1:def 1;

hence ex f being Function st

( f = the Comp of F . (f,g,h) & f . (t2,t1) = t2 `*` t1 ) by A65; :: thesis: verum