let C1, C2 be non empty category; for f being morphism of (Functors (C1,C2)) ex F1, F2 being covariant Functor of C1,C2 ex T being natural_transformation of F1,F2 st
( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )
set C = Functors (C1,C2);
let f be morphism of (Functors (C1,C2)); ex F1, F2 being covariant Functor of C1,C2 ex T being natural_transformation of F1,F2 st
( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )
consider f1 being morphism of (Functors (C1,C2)) such that
A1:
( dom f = f1 & f |> f1 & f1 is identity )
by CAT_6:def 18;
consider f2 being morphism of (Functors (C1,C2)) such that
A2:
( cod f = f2 & f2 |> f & f2 is identity )
by CAT_6:def 19;
consider G1, G11, G12 being covariant Functor of C1,C2, T11 being natural_transformation of G11,G1, T12 being natural_transformation of G1,G12 such that
A3:
( f = [[G1,G12],T12] & f1 = [[G11,G1],T11] & f (*) f1 = [[G11,G12],(T12 `*` T11)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds
( T12 . g2 |> T11 . g1 & (T12 `*` T11) . (g2 (*) g1) = (T12 . g2) (*) (T11 . g1) ) ) )
by A1, Th63;
consider F1 being covariant Functor of C1,C2 such that
A4:
f1 = [[F1,F1],F1]
by A1, Th64;
[G11,G1] = [F1,F1]
by A3, A4, XTUPLE_0:1;
then A5:
G1 = F1
by XTUPLE_0:1;
consider G2, G21, G22 being covariant Functor of C1,C2, T21 being natural_transformation of G21,G2, T22 being natural_transformation of G2,G22 such that
A6:
( f2 = [[G2,G22],T22] & f = [[G21,G2],T21] & f2 (*) f = [[G21,G22],(T22 `*` T21)] & ( for g1, g2 being morphism of C1 st g2 |> g1 holds
( T22 . g2 |> T21 . g1 & (T22 `*` T21) . (g2 (*) g1) = (T22 . g2) (*) (T21 . g1) ) ) )
by A2, Th63;
consider F2 being covariant Functor of C1,C2 such that
A7:
f2 = [[F2,F2],F2]
by A2, Th64;
[G2,G22] = [F2,F2]
by A6, A7, XTUPLE_0:1;
then A8:
G2 = F2
by XTUPLE_0:1;
A9:
[G1,G12] = [G21,G2]
by A3, A6, XTUPLE_0:1;
then reconsider T = T12 as natural_transformation of F1,F2 by A5, A8, XTUPLE_0:1;
take
F1
; ex F2 being covariant Functor of C1,C2 ex T being natural_transformation of F1,F2 st
( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )
take
F2
; ex T being natural_transformation of F1,F2 st
( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )
take
T
; ( f = [[F1,F2],T] & dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )
thus
f = [[F1,F2],T]
by A3, A5, A9, A8, XTUPLE_0:1; ( dom f = [[F1,F1],F1] & cod f = [[F2,F2],F2] )
thus
dom f = [[F1,F1],F1]
by A1, A4; cod f = [[F2,F2],F2]
thus
cod f = [[F2,F2],F2]
by A2, A7; verum