defpred S₁[ set , set ] means for f, g being strict covariant Functor of A,B st [f,g] = $1 holds
for x being set holds
( x in $2 iff ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) );
A1: for i being set st i in [:(Funct A,B),(Funct A,B):] holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis:
assume i in [:(Funct A,B),(Funct A,B):] ; :: thesis:
then consider f, g being set such that
A2: ( f in Funct A,B & g in Funct A,B & 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₂[ set , set ] means ex o being object of A st
( $1 = o & $2 = <^(f . o),(g . o)^> );
A3: for a being Element of A ex j being set st S₂[a,j]

proof

let a be Element of A; :: thesis:
reconsider o = a as object of A ;
consider j being set such that
A4: j = <^(f . o),(g . o)^> ;
thus ex j being set st S₂[a,j] by A4; :: thesis:

end;

consider N being ManySortedSet of such that
A5: for a being Element of A holds S₂[a,N . a] from PBOOLE:sch 6(A3);
defpred S₃[ set ] means ( f is_naturally_transformable_to g & $1 is natural_transformation of f,g );
consider j being set such that
A6: for x being set holds
( x in j iff ( x in product N & S₃[x] ) ) from XBOOLE_0:sch 1();
take j ; :: thesis:
let f', g' be strict covariant Functor of A,B; :: thesis:
assume A7: [f',g'] = i ; :: thesis:
let x be set ; :: thesis:
thus ( x in j implies ( f' is_naturally_transformable_to g' & x is natural_transformation of f',g' ) ) :: thesis:

proof

assume A8: x in j ; :: thesis:
( f' = f & g' = g ) by A2, A7, ZFMISC_1:33;
hence ( f' is_naturally_transformable_to g' & x is natural_transformation of f',g' ) by A6, A8; :: thesis:

end;

thus ( f' is_naturally_transformable_to g' & x is natural_transformation of f',g' implies x in j ) :: thesis:

proof

assume A9: ( f' is_naturally_transformable_to g' & x is natural_transformation of f',g' ) ; :: thesis:
then A10: f' is_transformable_to g' by Def6;
A11: ( f' = f & g' = g ) by A2, A7, ZFMISC_1:33;
reconsider h = x as ManySortedSet of by A9;
A12: dom h = the carrier of A by PARTFUN1:def 4;
set I = the carrier of A;
A13: for i' being set st i' in the carrier of A holds
h . i' in N . i'

proof

let i' be set ; :: thesis:
assume i' in the carrier of A ; :: thesis:
then reconsider i' = i' as Element of A ;
consider i'' being object of A such that
A14: i'' = i' and
A15: N . i' = <^(f . i''),(g . i'')^> by A5;
A16: <^(f . i''),(g . i'')^> <> {} by A10, A11, Def1;
h . i'' is Element of <^(f . i''),(g . i'')^> by A9, A10, A11, Def2;
hence h . i' in N . i' by A14, A15, A16; :: thesis:

end;

A17: for i' being set st i' in dom N holds
h . i' in N . i'

proof

let i' be set ; :: thesis:
assume A18: i' in dom N ; :: thesis:
dom N = the carrier of A by PARTFUN1:def 4;
hence h . i' in N . i' by A13, A18; :: thesis:

end;

dom h = dom N by A12, PARTFUN1:def 4;
then x in product N by A17, CARD_3:18;
hence x in j by A6, A9, A11; :: thesis:

end;

consider a being ManySortedSet of such that
A19: for i being set st i in [:(Funct A,B),(Funct A,B):] holds
S₁[i,a . i] from PBOOLE:sch 3(A1);
defpred S₂[ set , set , set ] 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;
A20: for o being set st o in [:(Funct A,B),(Funct A,B),(Funct A,B):] holds
for x being set st x in {|a,a|} . o holds
ex y being set st
( y in {|a|} . o & S₂[y,x,o] )

proof

let o be set ; :: thesis:
assume o in [:(Funct A,B),(Funct A,B),(Funct A,B):] ; :: thesis:
then o in [:[:(Funct A,B),(Funct A,B):],(Funct A,B):] by ZFMISC_1:def 3;
then consider ff, h being set such that
A21: ff in [:(Funct A,B),(Funct A,B):] and
A22: h in Funct A,B and
A23: o = [ff,h] by ZFMISC_1:def 2;
consider f, g being set such that
A24: f in Funct A,B and
A25: g in Funct A,B and
A26: ff = [f,g] by A21, ZFMISC_1:def 2;
A27: o = [f,g,h] by A23, A26, MCART_1:def 3;
reconsider T = Funct A,B as non empty set by A22;
reconsider i = f, j = g, k = h as Element of T by A22, A24, A25;
A28: {|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 6 ;
A29: {|a|} . [i,j,k] = {|a|} . i,j,k by MULTOP_1:def 1
.= a . i,k by ALTCAT_1:def 5 ;
for x being set st x in {|a,a|} . o holds
ex y being set st
( y in {|a|} . o & S₂[y,x,o] )

proof

let x be set ; :: thesis:
assume x in {|a,a|} . o ; :: thesis:
then consider x2, x1 being set such that
A30: x2 in a . j,k and
A31: x1 in a . i,j and
A32: x = [x2,x1] by A27, A28, ZFMISC_1:def 2;
A33: x2 in a . [j,k] by A30;
A34: x1 in a . [i,j] by A31;
reconsider i' = i, j' = j, k' = k as strict covariant Functor of A,B by Def10;
A35: ( i' is_naturally_transformable_to j' & x1 is natural_transformation of i',j' ) by A19, A34;
reconsider x1 = x1 as natural_transformation of i',j' by A19, A34;
A36: ( j' is_naturally_transformable_to k' & x2 is natural_transformation of j',k' ) by A19, A33;
reconsider x2 = x2 as natural_transformation of j',k' by A19, A33;
reconsider vv = x2 `*` x1 as natural_transformation of i',k' ;
A37: ( i' is_naturally_transformable_to k' & vv is natural_transformation of i',k' ) by A35, A36, Th10;
[i',k'] in [:(Funct A,B),(Funct A,B):] by ZFMISC_1:def 2;
then A38: vv in a . [i',k'] by A19, A37;
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

let f, g, h be strict covariant Functor of A,B; :: thesis:
assume A39: [f,g,h] = o ; :: thesis:
let t1 be natural_transformation of f,g; :: thesis:
let t2 be natural_transformation of g,h; :: thesis:
assume that
A40: [t2,t1] = x and
ex v being Function st v . x = vv ; :: thesis:
A41: ( i' = f & j' = g & k' = h ) by A27, A39, MCART_1:28;
then reconsider x1 = x1 as natural_transformation of f,g ;
reconsider x2 = x2 as natural_transformation of g,h by A41;
( x2 = t2 & x1 = t1 ) by A32, A40, ZFMISC_1:33;
hence vv = t2 `*` t1 by A41; :: thesis:

end;

hence ex y being set st
( y in {|a|} . o & S₂[y,x,o] ) by A27, A29, A38; :: thesis:

end;

hence for x being set st x in {|a,a|} . o holds
ex y being set st
( y in {|a|} . o & S₂[y,x,o] ) ; :: thesis:

end;

consider c being ManySortedFunction of {|a,a|},{|a|} such that
A42: for i being set 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 set st x in {|a,a|} . i holds
S₂[v . x,x,i] ) ) from MSSUBFAM:sch 1(A20);
set F = AltCatStr(# (Funct A,B),a,c #);
A43: not Funct A,B is empty

proof

consider f being strict covariant Functor of A,B;
f in Funct A,B by Def10;
hence not Funct A,B is empty ; :: thesis:

end;

AltCatStr(# (Funct A,B),a,c #) is transitive

proof

let o1, o2, o3 be object of AltCatStr(# (Funct A,B),a,c #); :: according to ALTCAT_1:def 4 :: thesis:
assume A44: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis:
reconsider a1 = o1, a2 = o2, a3 = o3 as strict covariant Functor of A,B by A43, Def10;
A45: [o1,o2] in [:(Funct A,B),(Funct A,B):] by A43, ZFMISC_1:def 2;
consider y being set such that
A46: y in a . [o1,o2] by A44, XBOOLE_0:def 1;
A47: ( a1 is_naturally_transformable_to a2 & y is natural_transformation of a1,a2 ) by A19, A45, A46;
reconsider y = y as natural_transformation of a1,a2 by A19, A45, A46;
A48: [o2,o3] in [:(Funct A,B),(Funct A,B):] by A43, ZFMISC_1:def 2;
consider x being set such that
A49: x in a . [o2,o3] by A44, XBOOLE_0:def 1;
A50: ( a2 is_naturally_transformable_to a3 & x is natural_transformation of a2,a3 ) by A19, A48, A49;
reconsider x = x as natural_transformation of a2,a3 by A19, A48, A49;
A51: x `*` y is natural_transformation of a1,a3 ;
A52: [o1,o3] in [:(Funct A,B),(Funct A,B):] by A43, ZFMISC_1:def 2;
( a1 is_naturally_transformable_to a3 & ex x being set st x is natural_transformation of a1,a3 ) by A47, A50, A51, Th10;
hence not <^o1,o3^> = {} by A19, A52; :: thesis:

end;

then reconsider F = AltCatStr(# (Funct A,B),a,c #) as non empty transitive strict AltCatStr by A43;
take F ; :: thesis:
thus the carrier of F = Funct A,B ; :: thesis:
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:

proof

let f, g be strict covariant Functor of A,B; :: thesis:
let x be set ; :: thesis:
thus ( x in the Arrows of F . f,g implies ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ) :: thesis:

proof

assume A53: x in the Arrows of F . f,g ; :: thesis:
( f in Funct A,B & g in Funct A,B ) by Def10;
then [f,g] in [:(Funct A,B),(Funct A,B):] by ZFMISC_1:def 2;
hence ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) by A19, A53; :: thesis:

end;

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

proof

assume A54: ( f is_naturally_transformable_to g & x is natural_transformation of f,g ) ; :: thesis:
( f in Funct A,B & g in Funct A,B ) by Def10;
then [f,g] in [:(Funct A,B),(Funct A,B):] by ZFMISC_1:106;
hence x in the Arrows of F . f,g by A19, A54; :: thesis:

end;

let f, g, h be strict covariant Functor of A,B; :: thesis:
assume A55: ( f is_naturally_transformable_to g & g is_naturally_transformable_to h ) ; :: thesis:
let t1 be natural_transformation of f,g; :: thesis:
let t2 be natural_transformation of g,h; :: thesis:
A56: ( f in Funct A,B & g in Funct A,B & h in Funct A,B ) by Def10;
A57: [:(Funct A,B),(Funct A,B),(Funct A,B):] = [:[:(Funct A,B),(Funct A,B):],(Funct A,B):] by ZFMISC_1:def 3;
A58: [f,g,h] = [[f,g],h] by MCART_1:def 3;
A59: [g,h] in [:(Funct A,B),(Funct A,B):] by A56, ZFMISC_1:106;
A60: [f,g] in [:(Funct A,B),(Funct A,B):] by A56, ZFMISC_1:106;
then [f,g,h] in [:(Funct A,B),(Funct A,B),(Funct A,B):] by A56, A57, A58, ZFMISC_1:106;
then consider v being Function of ({|a,a|} . [f,g,h]),({|a|} . [f,g,h]) such that
A61: v = c . [f,g,h] and
A62: for x being set st x in {|a,a|} . [f,g,h] holds
S₂[v . x,x,[f,g,h]] by A42;
A63: v = c . f,g,h by A61, MULTOP_1:def 1;
reconsider T = Funct A,B as non empty set by A56;
reconsider i = f, j = g, k = h as Element of T by Def10;
A64: {|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 6 ;
A65: t1 in a . [f,g] by A19, A55, A60;
t2 in a . [g,h] by A19, A55, A59;
then [t2,t1] in {|a,a|} . [f,g,h] by A64, A65, ZFMISC_1:106;
then v . t2,t1 = t2 `*` t1 by A62;
hence ex f being Function st
( f = the Comp of F . f,g,h & f . t2,t1 = t2 `*` t1 ) by A63; :: thesis: