let C1, C2 be non empty category; :: thesis:
let f1, f2 be morphism of (Functors (C1,C2)); :: thesis:
A1: the composition of (Functors (C1,C2)) = { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of (Functors (C1,C2)) : 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)] ) } by Def28;
thus ( f1 |> f2 implies ex F, F1, F2 being covariant Functor of C1,C2 ex T1 being natural_transformation of F1,F ex T2 being natural_transformation of F,F2 st
( f1 = [[F,F2],T2] & f2 = [[F1,F],T1] & f1 (*) f2 = [[F1,F2],(T2 `*` T1)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds
( T2 . g2 |> T1 . g1 & (T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) ) ) :: thesis:

proof

assume A2: f1 |> f2 ; :: thesis:
then A3: KuratowskiPair (f1,f2) in dom the composition of (Functors (C1,C2)) by CAT_6:def 2;
the composition of (Functors (C1,C2)) . (KuratowskiPair (f1,f2)) = the composition of (Functors (C1,C2)) . (f1,f2) by BINOP_1:def 1
.= f1 (*) f2 by A2, CAT_6:def 3 ;
then [(KuratowskiPair (f1,f2)),(f1 (*) f2)] in { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of (Functors (C1,C2)) : 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)] ) } by A1, A3, FUNCT_1:1;
then consider x1, x2, x3 being Element of the carrier of (Functors (C1,C2)) such that
A4: [(KuratowskiPair (f1,f2)),(f1 (*) f2)] = [[x2,x1],x3] and
A5: 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)] ) ;
consider F1, F, F2 being Functor of C1,C2, T1 being natural_transformation of F1,F, T2 being natural_transformation of F,F2 such that
A6: ( x1 = [[F1,F],T1] & x2 = [[F,F2],T2] & x3 = [[F1,F2],(T2 `*` T1)] ) by A5;
A7: the carrier of (Functors (C1,C2)) = { [[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 ) } by Def28;
x1 in the carrier of (Functors (C1,C2)) ;
then consider F11, F12 being Functor of C1,C2, T11 being natural_transformation of F11,F12 such that
A8: ( x1 = [[F11,F12],T11] & F11 is covariant & F12 is covariant & F11 is_naturally_transformable_to F12 ) by A7;
x2 in the carrier of (Functors (C1,C2)) ;
then consider F21, F22 being Functor of C1,C2, T21 being natural_transformation of F21,F22 such that
A9: ( x2 = [[F21,F22],T21] & F21 is covariant & F22 is covariant & F21 is_naturally_transformable_to F22 ) by A7;
A10: ( [F11,F12] = [F1,F] & [F21,F22] = [F,F2] ) by A8, A9, A6, XTUPLE_0:1;
then reconsider F = F, F1 = F1, F2 = F2 as covariant Functor of C1,C2 by A8, A9, XTUPLE_0:1;
reconsider T1 = T1 as natural_transformation of F1,F ;
reconsider T2 = T2 as natural_transformation of F,F2 ;
A11: ( KuratowskiPair (f1,f2) = [x2,x1] & f1 (*) f2 = x3 ) by A4, XTUPLE_0:1;
take F ; :: thesis:
take F1 ; :: thesis:
take F2 ; :: thesis:
take T1 ; :: thesis:
take T2 ; :: thesis:
thus f1 = [[F,F2],T2] by A6, A11, XTUPLE_0:1; :: thesis:
thus f2 = [[F1,F],T1] by A6, A11, XTUPLE_0:1; :: thesis:
thus f1 (*) f2 = [[F1,F2],(T2 `*` T1)] by A4, A6, XTUPLE_0:1; :: thesis:
let g1, g2 be morphism of C1; :: thesis:
assume A12: g2 |> g1 ; :: thesis:
consider g11, g12 being morphism of C1 such that
A13: ( g11 is identity & g12 is identity & g11 |> g1 & g1 |> g12 ) by Th5;
A14: ( F11 = F1 & F12 = F ) by A10, XTUPLE_0:1;
T1 is_natural_transformation_of F1,F by A14, A8, Def26;
then A15: ( T1 . g11 |> F1 . g1 & F . g1 |> T1 . g12 & T1 . g1 = (T1 . g11) (*) (F1 . g1) & T1 . g1 = (F . g1) (*) (T1 . g12) ) by A13, Th58;
consider g21, g22 being morphism of C1 such that
A16: ( g21 is identity & g22 is identity & g21 |> g2 & g2 |> g22 ) by Th5;
A17: ( F21 = F & F22 = F2 ) by A10, XTUPLE_0:1;
T2 is_natural_transformation_of F,F2 by A17, A9, Def26;
then A18: ( T2 . g21 |> F . g2 & F2 . g2 |> T2 . g22 & T2 . g2 = (T2 . g21) (*) (F . g2) & T2 . g2 = (F2 . g2) (*) (T2 . g22) ) by A16, Th58;
dom (F . g2) = cod (F . g1) by CAT_7:5, A12, Th13;
then dom (T2 . g2) = cod (F . g1) by A18, CAT_7:4;
then dom (T2 . g2) = cod (T1 . g1) by A15, CAT_7:4;
hence T2 . g2 |> T1 . g1 by CAT_7:5; :: thesis:
dom (g2 (*) g1) = dom g1 by A12, CAT_7:4
.= cod g12 by A13, CAT_7:5 ;
then A19: g2 (*) g1 |> g12 by CAT_7:5;
dom g21 = cod g2 by A16, CAT_7:5
.= cod (g2 (*) g1) by A12, CAT_7:4 ;
then A20: g21 |> g2 (*) g1 by CAT_7:5;
A21: ( F . (g2 (*) g1) = (F . g2) (*) (F . g1) & F . g2 |> F . g1 ) by A12, Th13;
thus (T2 `*` T1) . (g2 (*) g1) = ((T2 . g21) (*) (F . (g2 (*) g1))) (*) (T1 . g12) by A13, A19, A20, A16, A14, A8, A17, A9, Def27
.= (((T2 . g21) (*) (F . g2)) (*) (F . g1)) (*) (T1 . g12) by A18, A21, A15, Th2
.= (T2 . g2) (*) (T1 . g1) by A18, A21, A15, Th2 ; :: thesis:

end;

assume A22: ex F, F1, F2 being covariant Functor of C1,C2 ex T1 being natural_transformation of F1,F ex T2 being natural_transformation of F,F2 st
( f1 = [[F,F2],T2] & f2 = [[F1,F],T1] & f1 (*) f2 = [[F1,F2],(T2 `*` T1)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds
( T2 . g2 |> T1 . g1 & (T2 `*` T1) . (g2 (*) g1) = (T2 . g2) (*) (T1 . g1) ) ) ) ; :: thesis:
reconsider x1 = f2, x2 = f1, x3 = f1 (*) f2 as Element of the carrier of (Functors (C1,C2)) by CAT_6:def 1;
[[x2,x1],x3] in { [[x2,x1],x3] where x1, x2, x3 is Element of the carrier of (Functors (C1,C2)) : 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)] ) } by A22;
then KuratowskiPair (f1,f2) in dom the composition of (Functors (C1,C2)) by A1, XTUPLE_0:def 12;
hence f1 |> f2 by CAT_6:def 2; :: thesis: