let C, D be Category; :: thesis: for F1, F2 being Functor of C,D
for G1, G2, T being Functor of (alter C),(alter D) st F1 = G1 & F2 = G2 & T is_natural_transformation_of G1,G2 holds
(IdMap C) * T is natural_transformation of F1,F2
let F1, F2 be Functor of C,D; :: thesis: for G1, G2, T being Functor of (alter C),(alter D) st F1 = G1 & F2 = G2 & T is_natural_transformation_of G1,G2 holds
(IdMap C) * T is natural_transformation of F1,F2
let G1, G2, T be Functor of (alter C),(alter D); :: thesis: ( F1 = G1 & F2 = G2 & T is_natural_transformation_of G1,G2 implies (IdMap C) * T is natural_transformation of F1,F2 )
assume A1: ( F1 = G1 & F2 = G2 ) ; :: thesis: ( not T is_natural_transformation_of G1,G2 or (IdMap C) * T is natural_transformation of F1,F2 )
assume A2: T is_natural_transformation_of G1,G2 ; :: thesis: (IdMap C) * T is natural_transformation of F1,F2
A3: alter C = CategoryStr(# the carrier' of C, the Comp of C #) by CAT_6:def 34;
A4: alter D = CategoryStr(# the carrier' of D, the Comp of D #) by CAT_6:def 34;
A5: for a being Object of C holds T . (id a) in Hom ((F1 . a),(F2 . a))

proof

let a be Object of C; :: thesis: T . (id a) in Hom ((F1 . a),(F2 . a))
reconsider f = id a as morphism of (alter C) by A3, CAT_6:def 1;
A6: f is identity by CAT_6:41;
f |> f by CAT_6:24, CAT_6:41;
then A7: ( T . f |> G1 . f & G2 . f |> T . f & T . (f (*) f) = (T . f) (*) (G1 . f) & T . (f (*) f) = (G2 . f) (*) (T . f) ) by A2;
reconsider g = T . f as Morphism of D by A4, CAT_6:def 1;
( G1 is covariant & G2 is covariant ) by A1, CAT_6:42;
then ( G1 is identity-preserving & G2 is identity-preserving ) by CAT_6:def 25;
then ( dom (T . f) = G1 . f & cod (T . f) = G2 . f ) by A7, CAT_6:26, CAT_6:27, A6, CAT_6:def 22;
then ( dom (T . f) = F1 . f & cod (T . f) = F2 . f ) by A1, CAT_6:def 21;
then ( F1 . f = id (dom g) & F2 . f = id (cod g) ) by Th14;
then A8: ( dom g = F1 . a & cod g = F2 . a ) by CAT_1:70;
g in Hom ((dom g),(cod g)) by CAT_1:1;
hence T . (id a) in Hom ((F1 . a),(F2 . a)) by A8, CAT_6:def 21; :: thesis: verum

end;

A9: for a being Object of C holds Hom ((F1 . a),(F2 . a)) <> {} by A5;
then A10: F1 is_transformable_to F2 by NATTRA_1:def 2;
reconsider T1 = T as Function of the carrier' of C, the carrier' of D by A3, A4;
reconsider t1 = (IdMap C) * T1 as Function of the carrier of C, the carrier' of D ;
A11: ex t being transformation of F1,F2 st
( t = (IdMap C) * T1 & ( for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) )

proof

for a being Object of C holds t1 . a is Morphism of F1 . a,F2 . a

proof

let a be Object of C; :: thesis: t1 . a is Morphism of F1 . a,F2 . a
a in the carrier of C ;
then A12: a in dom (IdMap C) by FUNCT_2:def 1;
t1 . a = T1 . ((IdMap C) . a) by A12, FUNCT_1:13
.= T . (id a) by ISOCAT_1:def 12 ;
then t1 . a in Hom ((F1 . a),(F2 . a)) by A5;
hence t1 . a is Morphism of F1 . a,F2 . a by CAT_1:def 5; :: thesis: verum

end;

then reconsider t = t1 as transformation of F1,F2 by A10, NATTRA_1:def 3;
take t ; :: thesis: ( t = (IdMap C) * T1 & ( for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) )
thus t = (IdMap C) * T1 ; :: thesis: for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a)
let a, b be Object of C; :: thesis: ( Hom (a,b) <> {} implies for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) )
assume A13: Hom (a,b) <> {} ; :: thesis: for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a)
let f be Morphism of a,b; :: thesis: (t . b) * (F1 /. f) = (F2 /. f) * (t . a)
a in the carrier of C ;
then A14: a in dom (IdMap C) by FUNCT_2:def 1;
A15: t . a = t1 . a by A9, NATTRA_1:def 5, NATTRA_1:def 2
.= T1 . ((IdMap C) . a) by A14, FUNCT_1:13
.= T . (id a) by ISOCAT_1:def 12 ;
b in the carrier of C ;
then A16: b in dom (IdMap C) by FUNCT_2:def 1;
A17: t . b = t1 . b by A9, NATTRA_1:def 5, NATTRA_1:def 2
.= T1 . ((IdMap C) . b) by A16, FUNCT_1:13
.= T . (id b) by ISOCAT_1:def 12 ;
reconsider g2 = id a as morphism of (alter C) by A3, CAT_6:def 1;
reconsider g1 = id b as morphism of (alter C) by A3, CAT_6:def 1;
reconsider g = f as morphism of (alter C) by A3, CAT_6:def 1;
A18: f in Hom (a,b) by A13, CAT_1:def 5;
cod f = dom (id b) by A18, CAT_1:1;
then A19: KuratowskiPair (g1,g) in dom the composition of (alter C) by A3, CAT_1:def 6;
then A20: g1 |> g by CAT_6:def 2;
dom f = cod (id a) by A18, CAT_1:1;
then A21: KuratowskiPair (g,g2) in dom the composition of (alter C) by A3, CAT_1:def 6;
then A22: g |> g2 by CAT_6:def 2;
A23: for g being morphism of (alter C) st g1 |> g holds
g1 (*) g = g

proof

let g be morphism of (alter C); :: thesis: ( g1 |> g implies g1 (*) g = g )
assume A24: g1 |> g ; :: thesis: g1 (*) g = g
reconsider f = g as Morphism of C by A3, CAT_6:def 1;
A25: [(id b),f] in dom the Comp of C by A3, A24, CAT_6:def 2;
then dom (id b) = cod f by CAT_1:15;
then (id b) (*) f = f by CAT_1:21;
hence g1 (*) g = g by A25, CAT_6:40; :: thesis: verum

end;

A26: for g being morphism of (alter C) st g |> g2 holds
g (*) g2 = g

proof

let g be morphism of (alter C); :: thesis: ( g |> g2 implies g (*) g2 = g )
assume A27: g |> g2 ; :: thesis: g (*) g2 = g
reconsider f = g as Morphism of C by A3, CAT_6:def 1;
A28: [f,(id a)] in dom the Comp of C by A3, A27, CAT_6:def 2;
then cod (id a) = dom f by CAT_1:15;
then f (*) (id a) = f by CAT_1:22;
hence g (*) g2 = g by A28, CAT_6:40; :: thesis: verum

end;

A29: ( T . g1 |> G1 . g & G2 . g |> T . g2 & T . (g1 (*) g) = (T . g1) (*) (G1 . g) & T . (g (*) g2) = (G2 . g) (*) (T . g2) ) by A20, A22, A2;
A30: ( g1 (*) g = g & g (*) g2 = g ) by A19, A21, A23, A26, CAT_6:def 2;
A31: Hom ((F1 . b),(F2 . b)) <> {} by A5;
A32: Hom ((F1 . a),(F1 . b)) <> {} by A13, CAT_1:82;
A33: Hom ((F1 . a),(F2 . a)) <> {} by A5;
A34: Hom ((F2 . a),(F2 . b)) <> {} by A13, CAT_1:82;
A35: t . b = T . g1 by A17, CAT_6:def 21;
A36: F1 . f = G1 . g by A1, CAT_6:def 21;
A37: t . a = T . g2 by A15, CAT_6:def 21;
A38: F2 . f = G2 . g by A1, CAT_6:def 21;
A39: [(t . b),(F1 . f)] in dom the Comp of D by A35, A36, A4, A29, CAT_6:def 2;
A40: [(F2 . f),(t . a)] in dom the Comp of D by A37, A38, A4, A29, CAT_6:def 2;
thus (t . b) * (F1 /. f) = (t . b) (*) (F1 /. f) by A31, A32, CAT_1:def 13
.= (t . b) (*) (F1 . f) by A13, CAT_3:def 10
.= the Comp of D . ((t . b),(F1 . f)) by A39, CAT_1:def 1
.= the composition of (alter D) . ((T . g1),(G1 . g)) by A36, A4, A17, CAT_6:def 21
.= (T . g1) (*) (G1 . g) by A29, CAT_6:def 3
.= the composition of (alter D) . ((G2 . g),(T . g2)) by A30, A29, CAT_6:def 3
.= the Comp of D . ((F2 . f),(t . a)) by A38, A4, A15, CAT_6:def 21
.= (F2 . f) (*) (t . a) by A40, CAT_1:def 1
.= (F2 /. f) (*) (t . a) by A13, CAT_3:def 10
.= (F2 /. f) * (t . a) by A33, A34, CAT_1:def 13 ; :: thesis: verum

end;

then A41: F1 is_naturally_transformable_to F2 by A9, NATTRA_1:def 7, NATTRA_1:def 2;
consider t being transformation of F1,F2 such that
A42: ( t = (IdMap C) * T1 & ( for a, b being Object of C st Hom (a,b) <> {} holds
for f being Morphism of a,b holds (t . b) * (F1 /. f) = (F2 /. f) * (t . a) ) ) by A11;
thus (IdMap C) * T is natural_transformation of F1,F2 by A41, A42, NATTRA_1:def 8; :: thesis: verum