per cases ( ( not C1 is empty & C2 is empty ) or ( not C1 is empty & not C2 is empty ) or C1 is empty ) ;
suppose A1: ( not C1 is empty & C2 is empty ) ; :: thesis: ex b1 being strict category st
( the carrier of b1 = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b1 = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b1 : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )
set car = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } ;
reconsider car = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } as set ;
set comp = { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ;
for x being object st x in { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } holds
x in [:[:car,car:],car:] by A1, Lm4;
then reconsider comp = { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } as Relation of [:car,car:],car by TARSKI:def 3;
reconsider comp = comp as PartFunc of [:car,car:],car by A1, Lm4;
reconsider C = CategoryStr(# car,comp #) as CategoryStr ;
C is empty by A1, Lm4;
then reconsider C = C as strict category by CAT_6:def 11, CAT_6:def 12;
take C ; :: thesis: ( the carrier of C = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of C = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of C : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )
thus ( the carrier of C = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of C = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of C : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ) ; :: thesis: verum
end;
suppose A2: ( ( not C1 is empty & not C2 is empty ) or C1 is empty ) ; :: thesis: ex b1 being strict category st
( the carrier of b1 = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b1 = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b1 : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )
set car = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } ;
not { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } is empty
proof
per cases ( ( not C1 is empty & not C2 is empty ) or C1 is empty ) by A2;
suppose ( not C1 is empty & not C2 is empty ) ; :: thesis: not { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } is empty
then reconsider CA = C1, CB = C2 as non empty category ;
set F = the covariant Functor of CA,CB;
A3: the covariant Functor of CA,CB is_natural_transformation_of the covariant Functor of CA,CB, the covariant Functor of CA,CB by Th61;
the covariant Functor of CA,CB is_naturally_transformable_to the covariant Functor of CA,CB by Th61;
then reconsider T = the covariant Functor of CA,CB as natural_transformation of the covariant Functor of CA,CB, the covariant Functor of CA,CB by A3, Def26;
the covariant Functor of CA,CB is_naturally_transformable_to the covariant Functor of CA,CB by Th61;
then [[ the covariant Functor of CA,CB, the covariant Functor of CA,CB],T] in { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } ;
hence not { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } is empty ; :: thesis: verum
end;
suppose C1 is empty ; :: thesis: not { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } is empty
then reconsider CA = C1 as empty category ;
set F = the covariant Functor of CA,C2;
the covariant Functor of CA,C2 is_naturally_transformable_to the covariant Functor of CA,C2 by Th61;
then reconsider T = the covariant Functor of CA,C2 as natural_transformation of the covariant Functor of CA,C2, the covariant Functor of CA,C2 by Def26;
the covariant Functor of CA,C2 is_naturally_transformable_to the covariant Functor of CA,C2 by Th61;
then [[ the covariant Functor of CA,C2, the covariant Functor of CA,C2],T] in { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } ;
hence not { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } is empty ; :: thesis: verum
end;
end;
end;
then reconsider car = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } as non empty set ;
set comp = { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ;
for x being object st x in { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } holds
x in [:[:car,car:],car:]
proof
let x be object ; :: thesis: ( x in { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } implies x in [:[:car,car:],car:] )
assume x in { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ; :: thesis: x in [:[:car,car:],car:]
then consider x1, x2, x3 being Element of car such that
A4: ( x = [[x2,x1],x3] & ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) ) ;
[x2,x1] in [:car,car:] by ZFMISC_1:def 2;
hence x in [:[:car,car:],car:] by A4, ZFMISC_1:def 2; :: thesis: verum
end;
then reconsider comp = { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } as Relation of [:car,car:],car by TARSKI:def 3;
for x, y1, y2 being object st [x,y1] in comp & [x,y2] in comp holds
y1 = y2
proof
let x, y1, y2 be object ; :: thesis: ( [x,y1] in comp & [x,y2] in comp implies y1 = y2 )
assume [x,y1] in comp ; :: thesis: ( not [x,y2] in comp or y1 = y2 )
then consider x11, x12, x13 being Element of car such that
A5: ( [x,y1] = [[x12,x11],x13] & ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x11 = [[F1,F2],T1] & x12 = [[F2,F3],T2] & x13 = [[F1,F3],(T2 `*` T1)] ) ) ;
assume [x,y2] in comp ; :: thesis: y1 = y2
then consider x21, x22, x23 being Element of car such that
A6: ( [x,y2] = [[x22,x21],x23] & ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x21 = [[F1,F2],T1] & x22 = [[F2,F3],T2] & x23 = [[F1,F3],(T2 `*` T1)] ) ) ;
A7: ( x = [x12,x11] & y1 = x13 ) by A5, XTUPLE_0:1;
A8: ( x = [x22,x21] & y2 = x23 ) by A6, XTUPLE_0:1;
A9: ( x11 = x21 & x12 = x22 ) by A7, A8, XTUPLE_0:1;
consider F11, F12, F13 being Functor of C1,C2, T11 being natural_transformation of F11,F12, T12 being natural_transformation of F12,F13 such that
A10: ( x11 = [[F11,F12],T11] & x12 = [[F12,F13],T12] & x13 = [[F11,F13],(T12 `*` T11)] ) by A5;
consider F21, F22, F23 being Functor of C1,C2, T21 being natural_transformation of F21,F22, T22 being natural_transformation of F22,F23 such that
A11: ( x21 = [[F21,F22],T21] & x22 = [[F22,F23],T22] & x23 = [[F21,F23],(T22 `*` T21)] ) by A6;
A12: ( [F11,F12] = [F21,F22] & T21 = T11 ) by A10, A11, A9, XTUPLE_0:1;
then A13: ( F11 = F21 & F12 = F22 ) by XTUPLE_0:1;
A14: ( [F12,F13] = [F22,F23] & T22 = T12 ) by A10, A11, A9, XTUPLE_0:1;
then ( F12 = F22 & F13 = F23 ) by XTUPLE_0:1;
hence y1 = y2 by A5, XTUPLE_0:1, A6, A10, A11, A12, A13, A14; :: thesis: verum
end;
then reconsider comp = comp as PartFunc of [:car,car:],car by FUNCT_1:def 1;
reconsider C = CategoryStr(# car,comp #) as non empty CategoryStr ;
per cases ( ( not C1 is empty & not C2 is empty ) or C1 is empty ) by A2;
suppose ( not C1 is empty & not C2 is empty ) ; :: thesis: ex b1 being strict category st
( the carrier of b1 = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b1 = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b1 : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )
then reconsider CA = C1, CB = C2 as non empty category ;
A15: for g1, g2 being morphism of C st g1 |> g2 holds
ex F1, F2, F3 being Functor of CA,CB ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] & F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
proof
let g1, g2 be morphism of C; :: thesis: ( g1 |> g2 implies ex F1, F2, F3 being Functor of CA,CB ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] & F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] ) )
assume A16: g1 |> g2 ; :: thesis: ex F1, F2, F3 being Functor of CA,CB ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] & F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
g1 in Mor C ;
then g1 in the carrier of C by CAT_6:def 1;
then consider F11, F12 being Functor of CA,CB, T11 being natural_transformation of F11,F12 such that
A17: ( g1 = [[F11,F12],T11] & F11 is covariant & F12 is covariant & F11 is_naturally_transformable_to F12 ) ;
g2 in Mor C ;
then g2 in the carrier of C by CAT_6:def 1;
then consider F21, F22 being Functor of CA,CB, T22 being natural_transformation of F21,F22 such that
A18: ( g2 = [[F21,F22],T22] & F21 is covariant & F22 is covariant & F21 is_naturally_transformable_to F22 ) ;
[g1,g2] in dom the composition of C by A16, CAT_6:def 2;
then consider y being object such that
A19: [[g1,g2],y] in comp by XTUPLE_0:def 12;
consider x1, x2, x3 being Element of car such that
A20: ( [[g1,g2],y] = [[x2,x1],x3] & ex F1, F2, F3 being Functor of CA,CB ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) ) by A19;
consider F1, F2, F3 being Functor of CA,CB, T1 being natural_transformation of F1,F2, T2 being natural_transformation of F2,F3 such that
A21: ( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) by A20;
A22: ( [g1,g2] = [x2,x1] & y = x3 ) by A20, XTUPLE_0:1;
then A23: ( g1 = x2 & g2 = x1 ) by XTUPLE_0:1;
take F1 ; :: thesis: ex F2, F3 being Functor of CA,CB ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] & F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
take F2 ; :: thesis: ex F3 being Functor of CA,CB ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] & F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
take F3 ; :: thesis: ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] & F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
take T1 ; :: thesis: ex T2 being natural_transformation of F2,F3 st
( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] & F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
take T2 ; :: thesis: ( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] & F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
thus ( g1 = [[F2,F3],T2] & g2 = [[F1,F2],T1] ) by A21, A22, XTUPLE_0:1; :: thesis: ( F1 is covariant & F2 is covariant & F3 is covariant & F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
A24: ( [F11,F12] = [F2,F3] & [F21,F22] = [F1,F2] ) by A17, A18, A21, A23, XTUPLE_0:1;
then A25: ( F11 = F2 & F12 = F3 & F21 = F1 & F22 = F2 ) by XTUPLE_0:1;
thus ( F1 is covariant & F2 is covariant & F3 is covariant ) by A17, A18, A24, XTUPLE_0:1; :: thesis: ( F1 is_naturally_transformable_to F2 & F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
thus F1 is_naturally_transformable_to F2 by A18, A25; :: thesis: ( F2 is_naturally_transformable_to F3 & g1 (*) g2 = [[F1,F3],(T2 `*` T1)] )
thus F2 is_naturally_transformable_to F3 by A17, A25; :: thesis: g1 (*) g2 = [[F1,F3],(T2 `*` T1)]
thus g1 (*) g2 = the composition of C . (g1,g2) by A16, CAT_6:def 3
.= the composition of C . [g1,g2] by BINOP_1:def 1
.= y by A19, FUNCT_1:1
.= [[F1,F3],(T2 `*` T1)] by A21, A20, XTUPLE_0:1 ; :: thesis: verum
end;
A26: for g1, g2 being morphism of C st ex F1, F2, F3, F4 being Functor of CA,CB ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F3,F4 st
( g1 = [[F1,F2],T1] & g2 = [[F3,F4],T2] & F2 = F3 & F1 is covariant & F2 is covariant & F4 is covariant & F1 is_naturally_transformable_to F2 & F3 is_naturally_transformable_to F4 ) holds
g2 |> g1
proof
let g1, g2 be morphism of C; :: thesis: ( ex F1, F2, F3, F4 being Functor of CA,CB ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F3,F4 st
( g1 = [[F1,F2],T1] & g2 = [[F3,F4],T2] & F2 = F3 & F1 is covariant & F2 is covariant & F4 is covariant & F1 is_naturally_transformable_to F2 & F3 is_naturally_transformable_to F4 ) implies g2 |> g1 )
given F1, F2, F3, F4 being Functor of CA,CB, T1 being natural_transformation of F1,F2, T2 being natural_transformation of F3,F4 such that A27: ( g1 = [[F1,F2],T1] & g2 = [[F3,F4],T2] & F2 = F3 & F1 is covariant & F2 is covariant & F4 is covariant & F1 is_naturally_transformable_to F2 & F3 is_naturally_transformable_to F4 ) ; :: thesis: g2 |> g1
A28: ( g1 in car & g2 in car ) by A27;
reconsider T2 = T2 as natural_transformation of F2,F4 by A27;
set g3 = [[F1,F4],(T2 `*` T1)];
F1 is_naturally_transformable_to F4 by A27, Th62;
then A29: [[F1,F4],(T2 `*` T1)] in car by A27;
[[g2,g1],[[F1,F4],(T2 `*` T1)]] in comp by A27, A28, A29;
then [g2,g1] in dom comp by XTUPLE_0:def 12;
hence g2 |> g1 by CAT_6:def 2; :: thesis: verum
end;
for g, g1, g2 being morphism of C st g1 |> g2 holds
( g1 (*) g2 |> g iff g2 |> g )
proof
let g, g1, g2 be morphism of C; :: thesis: ( g1 |> g2 implies ( g1 (*) g2 |> g iff g2 |> g ) )
assume g1 |> g2 ; :: thesis: ( g1 (*) g2 |> g iff g2 |> g )
then consider F11, F12, F13 being Functor of C1,C2, T11 being natural_transformation of F11,F12, T12 being natural_transformation of F12,F13 such that
A30: ( g1 = [[F12,F13],T12] & g2 = [[F11,F12],T11] & F11 is covariant & F12 is covariant & F13 is covariant & F11 is_naturally_transformable_to F12 & F12 is_naturally_transformable_to F13 & g1 (*) g2 = [[F11,F13],(T12 `*` T11)] ) by A15;
hereby :: thesis: ( g2 |> g implies g1 (*) g2 |> g )
assume g1 (*) g2 |> g ; :: thesis: g2 |> g
then consider F01, F02, F03 being Functor of C1,C2, T01 being natural_transformation of F01,F02, T02 being natural_transformation of F02,F03 such that
A31: ( g1 (*) g2 = [[F02,F03],T02] & g = [[F01,F02],T01] & F01 is covariant & F02 is covariant & F03 is covariant & F01 is_naturally_transformable_to F02 & F02 is_naturally_transformable_to F03 & (g1 (*) g2) (*) g = [[F01,F03],(T02 `*` T01)] ) by A15;
( [F11,F13] = [F02,F03] & T12 `*` T11 = T02 ) by A30, A31, XTUPLE_0:1;
then ( F11 = F02 & F13 = F03 ) by XTUPLE_0:1;
hence g2 |> g by A26, A30, A31; :: thesis: verum
end;
assume g2 |> g ; :: thesis: g1 (*) g2 |> g
then consider F01, F02, F03 being Functor of C1,C2, T01 being natural_transformation of F01,F02, T02 being natural_transformation of F02,F03 such that
A32: ( g2 = [[F02,F03],T02] & g = [[F01,F02],T01] & F01 is covariant & F02 is covariant & F03 is covariant & F01 is_naturally_transformable_to F02 & F02 is_naturally_transformable_to F03 & g2 (*) g = [[F01,F03],(T02 `*` T01)] ) by A15;
( [F11,F12] = [F02,F03] & T11 = T02 ) by A30, A32, XTUPLE_0:1;
then A33: ( F11 = F02 & F12 = F03 ) by XTUPLE_0:1;
F11 is_naturally_transformable_to F13 by A30, Th62;
hence g1 (*) g2 |> g by A26, A30, A32, A33; :: thesis: verum
end;
then A34: C is left_composable by CAT_6:def 8;
A35: for g, g1, g2 being morphism of C st g1 |> g2 holds
( g |> g1 (*) g2 iff g |> g1 )
proof
let g, g1, g2 be morphism of C; :: thesis: ( g1 |> g2 implies ( g |> g1 (*) g2 iff g |> g1 ) )
assume g1 |> g2 ; :: thesis: ( g |> g1 (*) g2 iff g |> g1 )
then consider F11, F12, F13 being Functor of C1,C2, T11 being natural_transformation of F11,F12, T12 being natural_transformation of F12,F13 such that
A36: ( g1 = [[F12,F13],T12] & g2 = [[F11,F12],T11] & F11 is covariant & F12 is covariant & F13 is covariant & F11 is_naturally_transformable_to F12 & F12 is_naturally_transformable_to F13 & g1 (*) g2 = [[F11,F13],(T12 `*` T11)] ) by A15;
hereby :: thesis: ( g |> g1 implies g |> g1 (*) g2 )
assume g |> g1 (*) g2 ; :: thesis: g |> g1
then consider F01, F02, F03 being Functor of C1,C2, T01 being natural_transformation of F01,F02, T02 being natural_transformation of F02,F03 such that
A37: ( g = [[F02,F03],T02] & g1 (*) g2 = [[F01,F02],T01] & F01 is covariant & F02 is covariant & F03 is covariant & F01 is_naturally_transformable_to F02 & F02 is_naturally_transformable_to F03 & g (*) (g1 (*) g2) = [[F01,F03],(T02 `*` T01)] ) by A15;
( [F11,F13] = [F01,F02] & T12 `*` T11 = T01 ) by A36, A37, XTUPLE_0:1;
then ( F11 = F01 & F13 = F02 ) by XTUPLE_0:1;
hence g |> g1 by A26, A36, A37; :: thesis: verum
end;
assume g |> g1 ; :: thesis: g |> g1 (*) g2
then consider F01, F02, F03 being Functor of C1,C2, T01 being natural_transformation of F01,F02, T02 being natural_transformation of F02,F03 such that
A38: ( g = [[F02,F03],T02] & g1 = [[F01,F02],T01] & F01 is covariant & F02 is covariant & F03 is covariant & F01 is_naturally_transformable_to F02 & F02 is_naturally_transformable_to F03 & g (*) g1 = [[F01,F03],(T02 `*` T01)] ) by A15;
( [F12,F13] = [F01,F02] & T12 = T01 ) by A36, A38, XTUPLE_0:1;
then A39: ( F12 = F01 & F13 = F02 ) by XTUPLE_0:1;
F11 is_naturally_transformable_to F13 by A36, Th62;
hence g |> g1 (*) g2 by A26, A36, A38, A39; :: thesis: verum
end;
for g1 being morphism of C st g1 in the carrier of C holds
ex g being morphism of C st
( g |> g1 & g is left_identity )
proof
let g1 be morphism of C; :: thesis: ( g1 in the carrier of C implies ex g being morphism of C st
( g |> g1 & g is left_identity ) )
assume g1 in the carrier of C ; :: thesis: ex g being morphism of C st
( g |> g1 & g is left_identity )
then consider F11, F12 being Functor of CA,CB, T11 being natural_transformation of F11,F12 such that
A40: ( g1 = [[F11,F12],T11] & F11 is covariant & F12 is covariant & F11 is_naturally_transformable_to F12 ) ;
A41: F12 is_natural_transformation_of F12,F12 by A40, Th61;
A42: F12 is_naturally_transformable_to F12 by A40, Th61;
then reconsider T = F12 as natural_transformation of F12,F12 by A41, Def26;
set g = [[F12,F12],T];
[[F12,F12],T] in car by A40, A42;
then reconsider g = [[F12,F12],T] as morphism of C by CAT_6:def 1;
take g ; :: thesis: ( g |> g1 & g is left_identity )
thus g |> g1 by A26, A40, A42; :: thesis: g is left_identity
for g1 being morphism of C st g |> g1 holds
g (*) g1 = g1
proof
let g1 be morphism of C; :: thesis: ( g |> g1 implies g (*) g1 = g1 )
assume g |> g1 ; :: thesis: g (*) g1 = g1
then consider F01, F02, F03 being Functor of CA,CB, T01 being natural_transformation of F01,F02, T02 being natural_transformation of F02,F03 such that
A43: ( g = [[F02,F03],T02] & g1 = [[F01,F02],T01] & F01 is covariant & F02 is covariant & F03 is covariant & F01 is_naturally_transformable_to F02 & F02 is_naturally_transformable_to F03 & g (*) g1 = [[F01,F03],(T02 `*` T01)] ) by A15;
A44: ( [F02,F03] = [F12,F12] & T = T02 ) by A43, XTUPLE_0:1;
then A45: ( F02 = F12 & F03 = F12 ) by XTUPLE_0:1;
for x being object st x in the carrier of CA holds
(T02 `*` T01) . x = T01 . x
proof
let x be object ; :: thesis: ( x in the carrier of CA implies (T02 `*` T01) . x = T01 . x )
assume A46: x in the carrier of CA ; :: thesis: (T02 `*` T01) . x = T01 . x
reconsider f = x as morphism of CA by A46, CAT_6:def 1;
consider f1 being morphism of CA such that
A47: ( f1 |> f & f1 is left_identity ) by A46, CAT_6:def 6, CAT_6:def 12;
consider f2 being morphism of CA such that
A48: ( f |> f2 & f2 is right_identity ) by A46, CAT_6:def 7, CAT_6:def 12;
( f2 is left_identity & f1 is right_identity ) by A47, A48, CAT_6:9;
then A49: ( f1 is identity & f2 is identity ) by A47, A48, CAT_6:def 14;
A50: T01 is_natural_transformation_of F01,F02 by A43, Def26;
T02 is_natural_transformation_of F02,F03 by A43, Def26;
then A51: ( T02 . f1 |> F02 . f & F03 . f |> T02 . f2 & T02 . f = (T02 . f1) (*) (F02 . f) & T02 . f = (F03 . f) (*) (T02 . f2) ) by A43, A47, A48, A49, Th58;
T02 is covariant by A43, A44, XTUPLE_0:1;
then A52: T02 . f1 is identity by A49, CAT_6:def 22, CAT_6:def 25;
thus (T02 `*` T01) . x = (T02 `*` T01) . f by CAT_6:def 21
.= ((T02 . f1) (*) (F02 . f)) (*) (T01 . f2) by A47, A48, A49, A43, Def27
.= (F02 . f) (*) (T01 . f2) by A52, A51, CAT_6:def 4, CAT_6:def 14
.= T01 . f by A43, A50, A47, A48, A49, Th58
.= T01 . x by CAT_6:def 21 ; :: thesis: verum
end;
hence g (*) g1 = g1 by A43, A45, FUNCT_2:12; :: thesis: verum
end;
hence g is left_identity by CAT_6:def 4; :: thesis: verum
end;
then A53: C is with_left_identities by CAT_6:def 6;
A54: for g1 being morphism of C st g1 in the carrier of C holds
ex g being morphism of C st
( g1 |> g & g is right_identity )
proof
let g1 be morphism of C; :: thesis: ( g1 in the carrier of C implies ex g being morphism of C st
( g1 |> g & g is right_identity ) )
assume g1 in the carrier of C ; :: thesis: ex g being morphism of C st
( g1 |> g & g is right_identity )
then consider F11, F12 being Functor of CA,CB, T11 being natural_transformation of F11,F12 such that
A55: ( g1 = [[F11,F12],T11] & F11 is covariant & F12 is covariant & F11 is_naturally_transformable_to F12 ) ;
A56: F11 is_natural_transformation_of F11,F11 by A55, Th61;
A57: F11 is_naturally_transformable_to F11 by A55, Th61;
then reconsider T = F11 as natural_transformation of F11,F11 by A56, Def26;
set g = [[F11,F11],T];
[[F11,F11],T] in car by A55, A57;
then reconsider g = [[F11,F11],T] as morphism of C by CAT_6:def 1;
take g ; :: thesis: ( g1 |> g & g is right_identity )
thus g1 |> g by A26, A55, A57; :: thesis: g is right_identity
for g1 being morphism of C st g1 |> g holds
g1 (*) g = g1
proof
let g1 be morphism of C; :: thesis: ( g1 |> g implies g1 (*) g = g1 )
assume g1 |> g ; :: thesis: g1 (*) g = g1
then consider F01, F02, F03 being Functor of CA,CB, T01 being natural_transformation of F01,F02, T02 being natural_transformation of F02,F03 such that
A58: ( g1 = [[F02,F03],T02] & g = [[F01,F02],T01] & F01 is covariant & F02 is covariant & F03 is covariant & F01 is_naturally_transformable_to F02 & F02 is_naturally_transformable_to F03 & g1 (*) g = [[F01,F03],(T02 `*` T01)] ) by A15;
A59: ( [F01,F02] = [F11,F11] & T01 = T ) by A58, XTUPLE_0:1;
then A60: ( F01 = F11 & F02 = F11 ) by XTUPLE_0:1;
for x being object st x in the carrier of CA holds
(T02 `*` T01) . x = T02 . x
proof
let x be object ; :: thesis: ( x in the carrier of CA implies (T02 `*` T01) . x = T02 . x )
assume A61: x in the carrier of CA ; :: thesis: (T02 `*` T01) . x = T02 . x
reconsider f = x as morphism of CA by A61, CAT_6:def 1;
consider f1 being morphism of CA such that
A62: ( f1 |> f & f1 is left_identity ) by A61, CAT_6:def 6, CAT_6:def 12;
consider f2 being morphism of CA such that
A63: ( f |> f2 & f2 is right_identity ) by A61, CAT_6:def 7, CAT_6:def 12;
( f2 is left_identity & f1 is right_identity ) by A62, A63, CAT_6:9;
then A64: ( f1 is identity & f2 is identity ) by A62, A63, CAT_6:def 14;
T01 is_natural_transformation_of F01,F02 by A58, Def26;
then A65: ( T01 . f1 |> F01 . f & F02 . f |> T01 . f2 & T01 . f = (T01 . f1) (*) (F01 . f) & T01 . f = (F02 . f) (*) (T01 . f2) ) by A58, A62, A63, A64, Th58;
T02 is_natural_transformation_of F02,F03 by A58, Def26;
then A66: ( T02 . f1 |> F02 . f & F03 . f |> T02 . f2 & T02 . f = (T02 . f1) (*) (F02 . f) & T02 . f = (F03 . f) (*) (T02 . f2) ) by A58, A62, A63, A64, Th58;
thus (T02 `*` T01) . x = (T02 `*` T01) . f by CAT_6:def 21
.= ((T02 . f1) (*) (F02 . f)) (*) (T01 . f2) by A62, A63, A64, A58, Def27
.= T02 . f by A59, A60, A66, A65, Th1
.= T02 . x by CAT_6:def 21 ; :: thesis: verum
end;
hence g1 (*) g = g1 by A58, A60, FUNCT_2:12; :: thesis: verum
end;
hence g is right_identity by CAT_6:def 5; :: thesis: verum
end;
for g1, g2, g3 being morphism of C st g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 holds
g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3
proof
let g1, g2, g3 be morphism of C; :: thesis: ( g1 |> g2 & g2 |> g3 & g1 (*) g2 |> g3 & g1 |> g2 (*) g3 implies g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
assume g1 |> g2 ; :: thesis: ( not g2 |> g3 or not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
then consider F01, F02, F03 being Functor of CA,CB, T01 being natural_transformation of F01,F02, T02 being natural_transformation of F02,F03 such that
A67: ( g1 = [[F02,F03],T02] & g2 = [[F01,F02],T01] & F01 is covariant & F02 is covariant & F03 is covariant & F01 is_naturally_transformable_to F02 & F02 is_naturally_transformable_to F03 & g1 (*) g2 = [[F01,F03],(T02 `*` T01)] ) by A15;
assume g2 |> g3 ; :: thesis: ( not g1 (*) g2 |> g3 or not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
then consider F11, F12, F13 being Functor of CA,CB, T11 being natural_transformation of F11,F12, T12 being natural_transformation of F12,F13 such that
A68: ( g2 = [[F12,F13],T12] & g3 = [[F11,F12],T11] & F11 is covariant & F12 is covariant & F13 is covariant & F11 is_naturally_transformable_to F12 & F12 is_naturally_transformable_to F13 & g2 (*) g3 = [[F11,F13],(T12 `*` T11)] ) by A15;
assume g1 (*) g2 |> g3 ; :: thesis: ( not g1 |> g2 (*) g3 or g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 )
then consider F21, F22, F23 being Functor of CA,CB, T21 being natural_transformation of F21,F22, T22 being natural_transformation of F22,F23 such that
A69: ( g1 (*) g2 = [[F22,F23],T22] & g3 = [[F21,F22],T21] & F21 is covariant & F22 is covariant & F23 is covariant & F21 is_naturally_transformable_to F22 & F22 is_naturally_transformable_to F23 & (g1 (*) g2) (*) g3 = [[F21,F23],(T22 `*` T21)] ) by A15;
assume g1 |> g2 (*) g3 ; :: thesis: g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3
then consider F31, F32, F33 being Functor of CA,CB, T31 being natural_transformation of F31,F32, T32 being natural_transformation of F32,F33 such that
A70: ( g1 = [[F32,F33],T32] & g2 (*) g3 = [[F31,F32],T31] & F31 is covariant & F32 is covariant & F33 is covariant & F31 is_naturally_transformable_to F32 & F32 is_naturally_transformable_to F33 & g1 (*) (g2 (*) g3) = [[F31,F33],(T32 `*` T31)] ) by A15;
( [F02,F03] = [F32,F33] & T02 = T32 ) by A67, A70, XTUPLE_0:1;
then A71: ( F02 = F32 & F03 = F33 ) by XTUPLE_0:1;
A72: ( [F01,F02] = [F12,F13] & T01 = T12 ) by A67, A68, XTUPLE_0:1;
then A73: ( F01 = F12 & F02 = F13 ) by XTUPLE_0:1;
A74: ( [F01,F03] = [F22,F23] & T02 `*` T01 = T22 ) by A67, A69, XTUPLE_0:1;
then A75: ( F01 = F22 & F03 = F23 ) by XTUPLE_0:1;
( [F11,F12] = [F21,F22] & T11 = T21 ) by A68, A69, XTUPLE_0:1;
then A76: ( F11 = F21 & F12 = F22 ) by XTUPLE_0:1;
( [F11,F13] = [F31,F32] & T12 `*` T11 = T31 ) by A68, A70, XTUPLE_0:1;
then A77: ( F11 = F31 & F13 = F32 ) by XTUPLE_0:1;
for x being object st x in the carrier of CA holds
(T32 `*` T31) . x = (T22 `*` T21) . x
proof
let x be object ; :: thesis: ( x in the carrier of CA implies (T32 `*` T31) . x = (T22 `*` T21) . x )
assume A78: x in the carrier of CA ; :: thesis: (T32 `*` T31) . x = (T22 `*` T21) . x
reconsider f = x as morphism of CA by A78, CAT_6:def 1;
consider f1 being morphism of CA such that
A79: ( f1 |> f & f1 is left_identity ) by A78, CAT_6:def 6, CAT_6:def 12;
consider f2 being morphism of CA such that
A80: ( f |> f2 & f2 is right_identity ) by A78, CAT_6:def 7, CAT_6:def 12;
A81: ( f2 is left_identity & f1 is right_identity ) by A79, A80, CAT_6:9;
then A82: ( f1 is identity & f2 is identity ) by A79, A80, CAT_6:def 14;
A83: ( f1 |> f1 & f2 |> f2 ) by A81, A79, A80, CAT_6:def 14, CAT_6:24;
A84: T31 . f2 = (T12 `*` T11) . f2 by A68, A70, XTUPLE_0:1
.= ((T12 . f2) (*) (F12 . f2)) (*) (T11 . f2) by A82, A83, A68, Def27 ;
A85: T22 . f1 = (T02 `*` T01) . f1 by A67, A69, XTUPLE_0:1
.= ((T02 . f1) (*) (F02 . f1)) (*) (T01 . f1) by A82, A83, A67, Def27 ;
A86: T02 is_natural_transformation_of F02,F03 by A67, Def26;
A87: T01 is_natural_transformation_of F01,F02 by A67, Def26;
then A88: ( T01 . f1 |> F01 . f & F02 . f |> T01 . f2 & T01 . f = (T01 . f1) (*) (F01 . f) & T01 . f = (F02 . f) (*) (T01 . f2) ) by A79, A80, A82, A67, Th58;
A89: ( CB is left_composable & CB is right_composable ) by CAT_6:def 11;
A90: ( f1 |> f1 & f2 |> f2 ) by A81, CAT_6:24, A79, A80, CAT_6:def 14;
A91: T12 is_natural_transformation_of F12,F13 by A68, Def26;
then A92: T12 . f2 |> F12 . f2 by A90;
A93: T01 is_natural_transformation_of F01,F02 by A67, Def26;
then A94: F02 . f1 |> T01 . f1 by A90;
T11 is_natural_transformation_of F11,F12 by A68, Def26;
then A95: F12 . f2 |> T11 . f2 by A90;
T02 is_natural_transformation_of F02,F03 by A67, Def26;
then A96: T02 . f1 |> F02 . f1 by A90;
A97: F32 . f |> T12 . f2 by A87, A73, A77, A72, A80;
A98: T02 . f1 |> F32 . f by A86, A73, A77, A79;
A99: T01 . f1 |> F22 . f by A87, A75, A79;
A100: F32 . f |> (T12 . f2) (*) (F12 . f2) by A97, A91, A90, A82, A68, Th58;
A101: (T02 . f1) (*) (F32 . f) |> (T12 . f2) (*) (F12 . f2) by A89, A98, A100, CAT_6:def 8;
A102: (T12 . f2) (*) (F12 . f2) |> T11 . f2 by A89, A92, A95, CAT_6:def 8;
A103: (F32 . f) (*) ((T12 . f2) (*) (F12 . f2)) = (F32 . f) (*) (T12 . f2) by A91, A90, A82, A68, Th58
.= (F02 . f) (*) (T01 . f2) by A72, A77, XTUPLE_0:1
.= (T01 . f1) (*) (F22 . f) by A88, A74, XTUPLE_0:1
.= ((F02 . f1) (*) (T01 . f1)) (*) (F22 . f) by A67, A93, A90, A82, Th58 ;
A104: ((T02 . f1) (*) (F32 . f)) (*) ((T12 . f2) (*) (F12 . f2)) = (T02 . f1) (*) (((F02 . f1) (*) (T01 . f1)) (*) (F22 . f)) by A103, A98, A100, Th1
.= (((T02 . f1) (*) (F02 . f1)) (*) (T01 . f1)) (*) (F22 . f) by A96, A94, A99, Th2 ;
thus (T32 `*` T31) . x = (T32 `*` T31) . f by CAT_6:def 21
.= ((T32 . f1) (*) (F32 . f)) (*) (T31 . f2) by A79, A80, A82, A70, Def27
.= ((T02 . f1) (*) (F32 . f)) (*) (((T12 . f2) (*) (F12 . f2)) (*) (T11 . f2)) by A84, A67, A70, XTUPLE_0:1
.= (((T02 . f1) (*) (F32 . f)) (*) ((T12 . f2) (*) (F12 . f2))) (*) (T11 . f2) by A101, A102, Th1
.= ((((T02 . f1) (*) (F02 . f1)) (*) (T01 . f1)) (*) (F22 . f)) (*) (T21 . f2) by A104, A68, A69, XTUPLE_0:1
.= (T22 `*` T21) . f by A79, A80, A82, A69, A85, Def27
.= (T22 `*` T21) . x by CAT_6:def 21 ; :: thesis: verum
end;
hence g1 (*) (g2 (*) g3) = (g1 (*) g2) (*) g3 by A69, A70, A71, A75, A76, A77, FUNCT_2:12; :: thesis: verum
end;
then reconsider C = C as strict category by A54, A53, A35, A34, CAT_6:def 10, CAT_6:def 11, CAT_6:def 12, CAT_6:def 7, CAT_6:def 9;
take C ; :: thesis: ( the carrier of C = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of C = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of C : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )
thus ( the carrier of C = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of C = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of C : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ) ; :: thesis: verum
end;
suppose A105: C1 is empty ; :: thesis: ex b1 being strict category st
( the carrier of b1 = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b1 = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b1 : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } )
reconsider x = [[{},{}],{}] as set by TARSKI:1;
( car = {x} & { [[x2,x1],x3] where x1, x2, x3 is Element of car : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } = {[[x,x],x]} ) by A105, Lm5;
then C is non empty category by Th8;
hence ex b1 being strict category st
( the carrier of b1 = { [[F1,F2],T] where F1, F2 is Functor of C1,C2, T is natural_transformation of F2,F1 : ( F1 is covariant & F2 is covariant & F1 is_naturally_transformable_to F2 ) } & the composition of b1 = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of b1 : ex F1, F2, F3 being Functor of C1,C2 ex T1 being natural_transformation of F1,F2 ex T2 being natural_transformation of F2,F3 st
( x1 = [[F1,F2],T1] & x2 = [[F2,F3],T2] & x3 = [[F1,F3],(T2 `*` T1)] ) } ) ; :: thesis: verum
end;
end;
end;
end;