defpred S1[ 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 S2[ 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 S2[i,j]
proof
let i be object ; :: thesis: ( i in [:(Funct (A,B)),(Funct (A,B)):] implies ex j being object st S2[i,j] )
assume i in [:(Funct (A,B)),(Funct (A,B)):] ; :: thesis: ex j being object st S2[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 S3[ Object of A, object ] means $2 = <^(f . $1),(g . $1)^>;
defpred S4[ 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 S3[a,j] ;
consider N being ManySortedSet of the carrier of A such that
A5: for a being Element of A holds S3[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 & S4[x] ) ) from XBOOLE_0:sch 1();
 take j ; :: thesis: S2[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 )
proof
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;
thus ( f9 is_naturally_transformable_to g9 & x is natural_transformation of f9,g9 implies x in j ) :: 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
proof
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: S3[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;
A15: for i9 being object st i9 in dom N holds
h . i9 in N . i9
proof
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;
dom h = the carrier of A by PARTFUN1:def 2;
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;
end;
consider a being ManySortedSet of [:(Funct (A,B)),(Funct (A,B)):] such that
A17: for i being object st i in [:(Funct (A,B)),(Funct (A,B)):] holds
S2[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 & S1[y,x,o] )
proof
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 & S1[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 & S1[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 & S1[y,x,o] )
proof
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 & S1[y,x,o] ) )
assume x in {|a,a|} . o ; :: thesis: ex y being object st
( y in {|a|} . o & S1[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: S2[[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;
S2[[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
proof
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;
S2[[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;
S2[[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 & S1[y,x,o] ) by A24, A25, A34; :: thesis: verum
end;
hence for x being object st x in {|a,a|} . o holds
ex y being object st
( y in {|a|} . o & S1[y,x,o] ) ; :: thesis: verum
end;
consider c being ManySortedFunction of {|a,a|},{|a|} such that
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
S1[v . x,x,i] ) ) from MSSUBFAM:sch 1(A18);
 set F = AltCatStr(# (Funct (A,B)),a,c #);
A41: not Funct (A,B) is empty
proof
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;
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 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: S2[[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: S2[[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 S2[[o1,o3],a . [o1,o3]] by A17;
hence not <^o1,o3^> = {} by A49, A50; :: thesis: verum
end;
then reconsider F = AltCatStr(# (Funct (A,B)),a,c #) as non empty transitive strict AltCatStr by A41;
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 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) )
proof
( 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 )
S2[[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;
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
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)
S2[[f,g],a . [f,g]] by A17, A53;
hence x in the Arrows of F . (f,g) by A54; :: thesis: verum
end;
end;
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
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 S2[[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
S1[v . x,x,[f,g,h]] by A40;
S2[[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