let A, B, C be Category; :: thesis: for F1, F2 being Functor of [:A,B:],C st export F1 is_naturally_transformable_to export F2 holds
for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
let F1, F2 be Functor of [:A,B:],C; :: thesis: ( export F1 is_naturally_transformable_to export F2 implies for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u ) )
assume A1: export F1 is_naturally_transformable_to export F2 ; :: thesis: for t being natural_transformation of export F1, export F2 holds
( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
let t be natural_transformation of export F1, export F2; :: thesis: ( F1 is_naturally_transformable_to F2 & ex u being natural_transformation of F1,F2 st t = export u )
defpred S₁[ object , object ] means for a being Object of A st $1 = a holds
t . a = [[((export F1) . a),((export F2) . a)],$2];

A2: now :: thesis: for o being object st o in the carrier of A holds
ex m being object st
( m in Funcs ( the carrier of B, the carrier' of C) & S₁[o,m] )

let o be object ; :: thesis: ( o in the carrier of A implies ex m being object st
( m in Funcs ( the carrier of B, the carrier' of C) & S₁[o,m] ) )
assume o in the carrier of A ; :: thesis: ex m being object st
( m in Funcs ( the carrier of B, the carrier' of C) & S₁[o,m] )
then reconsider a9 = o as Object of A ;
consider f1, f2 being Functor of B,C, tau being natural_transformation of f1,f2 such that
f1 is_naturally_transformable_to f2 and
A3: dom (t . a9) = f1 and
A4: ( cod (t . a9) = f2 & t . a9 = [[f1,f2],tau] ) by Th6;
reconsider m = tau as object ;
take m = m; :: thesis: ( m in Funcs ( the carrier of B, the carrier' of C) & S₁[o,m] )
thus m in Funcs ( the carrier of B, the carrier' of C) by FUNCT_2:8; :: thesis: S₁[o,m]
thus S₁[o,m] :: thesis: verum

proof

let a be Object of A; :: thesis: ( o = a implies t . a = [[((export F1) . a),((export F2) . a)],m] )
assume A5: o = a ; :: thesis: t . a = [[((export F1) . a),((export F2) . a)],m]
export F1 is_transformable_to export F2 by A1;
then A6: Hom (((export F1) . a),((export F2) . a)) <> {} ;
then (export F1) . a = f1 by A3, A5, CAT_1:5;
hence t . a = [[((export F1) . a),((export F2) . a)],m] by A4, A5, A6, CAT_1:5; :: thesis: verum

end;

end;

consider t9 being Function of the carrier of A,(Funcs ( the carrier of B, the carrier' of C)) such that
A7: for o being object st o in the carrier of A holds
S₁[o,t9 . o] from FUNCT_2:sch 1(A2);
reconsider u9 = uncurry t9 as Function of the carrier of [:A,B:], the carrier' of C ;

A8: now :: thesis: for ab being Object of [:A,B:] holds u9 . ab in Hom ((F1 . ab),(F2 . ab))

let ab be Object of [:A,B:]; :: thesis: u9 . ab in Hom ((F1 . ab),(F2 . ab))
consider a being Object of A, b being Object of B such that
A9: ab = [a,b] by DOMAIN_1:1;
( (export F1) . a = F1 ?- a & (export F2) . a = F2 ?- a ) by Th18;
then t . a = [[(F1 ?- a),(F2 ?- a)],(t9 . a)] by A7;
then [[(F1 ?- a),(F2 ?- a)],(t9 . a)] in the carrier' of (Functors (B,C)) ;
then [[(F1 ?- a),(F2 ?- a)],(t9 . a)] in NatTrans (B,C) by NATTRA_1:def 17;
then consider G1, G2 being Functor of B,C, t99 being natural_transformation of G1,G2 such that
A10: [[(F1 ?- a),(F2 ?- a)],(t9 . a)] = [[G1,G2],t99] and
A11: G1 is_naturally_transformable_to G2 by NATTRA_1:def 15;
A12: G1 is_transformable_to G2 by A11;
A13: [(F1 ?- a),(F2 ?- a)] = [G1,G2] by A10, XTUPLE_0:1;
A14: F1 . [a,b] = (F1 ?- a) . b by Th8
.= G1 . b by A13, XTUPLE_0:1 ;
A15: Hom ((G1 . b),(G2 . b)) <> {} by A11, ISOCAT_1:25;
A16: F2 . [a,b] = (F2 ?- a) . b by Th8
.= G2 . b by A13, XTUPLE_0:1 ;
u9 . (a,b) = (t9 . a) . b by Th2
.= t99 . b by A10, XTUPLE_0:1
.= t99 . b by A12, NATTRA_1:def 5 ;
hence u9 . ab in Hom ((F1 . ab),(F2 . ab)) by A9, A14, A16, A15, CAT_1:def 5; :: thesis: verum

end;

A17: F1 is_transformable_to F2 by A8;
u9 is transformation of F1,F2

proof

thus F1 is_transformable_to F2 by A17; :: according to NATTRA_1:def 3 :: thesis: for b₁ being Element of the carrier of [:A,B:] holds u9 . b₁ is Morphism of F1 . b₁,F2 . b₁
let a be Object of [:A,B:]; :: thesis: u9 . a is Morphism of F1 . a,F2 . a
u9 . a in Hom ((F1 . a),(F2 . a)) by A8;
hence u9 . a is Morphism of F1 . a,F2 . a by CAT_1:def 5; :: thesis: verum

end;

then reconsider u = u9 as transformation of F1,F2 ;

A18: now :: thesis: for ab1, ab2 being Object of [:A,B:] st Hom (ab1,ab2) <> {} holds
for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1)

reconsider FF1 = F1, FF2 = F2 as Function of [: the carrier' of A, the carrier' of B:], the carrier' of C ;
let ab1, ab2 be Object of [:A,B:]; :: thesis: ( Hom (ab1,ab2) <> {} implies for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1) )
assume A19: Hom (ab1,ab2) <> {} ; :: thesis: for f being Morphism of ab1,ab2 holds (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1)
A20: Hom ((F2 . ab1),(F2 . ab2)) <> {} by A19, CAT_1:84;
consider a2 being Object of A, b2 being Object of B such that
A21: ab2 = [a2,b2] by DOMAIN_1:1;
( (export F1) . a2 = F1 ?- a2 & (export F2) . a2 = F2 ?- a2 ) by Th18;
then t . a2 = [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] by A7;
then [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] in the carrier' of (Functors (B,C)) ;
then [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] in NatTrans (B,C) by NATTRA_1:def 17;
then consider G2, H2 being Functor of B,C, t2 being natural_transformation of G2,H2 such that
A22: [[(F1 ?- a2),(F2 ?- a2)],(t9 . a2)] = [[G2,H2],t2] and
A23: G2 is_naturally_transformable_to H2 by NATTRA_1:def 15;
A24: ( t9 . a2 = t2 & G2 is_transformable_to H2 ) by A22, A23, XTUPLE_0:1;
consider a1 being Object of A, b1 being Object of B such that
A25: ab1 = [a1,b1] by DOMAIN_1:1;
( (export F1) . a1 = F1 ?- a1 & (export F2) . a1 = F2 ?- a1 ) by Th18;
then t . a1 = [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] by A7;
then [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] in the carrier' of (Functors (B,C)) ;
then [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] in NatTrans (B,C) by NATTRA_1:def 17;
then consider G1, H1 being Functor of B,C, t1 being natural_transformation of G1,H1 such that
A26: [[(F1 ?- a1),(F2 ?- a1)],(t9 . a1)] = [[G1,H1],t1] and
A27: G1 is_naturally_transformable_to H1 by NATTRA_1:def 15;
A28: ( t9 . a1 = t1 & G1 is_transformable_to H1 ) by A26, A27, XTUPLE_0:1;
A29: u . ab1 = u9 . (a1,b1) by A17, A25, NATTRA_1:def 5
.= (t9 . a1) . b1 by Th2
.= t1 . b1 by A28, NATTRA_1:def 5 ;
A30: Hom ((G1 . b2),(H1 . b2)) <> {} by A27, ISOCAT_1:25;
A31: Hom ((F1 . ab1),(F1 . ab2)) <> {} by A19, CAT_1:84;
A32: Hom ((F1 . ab2),(F2 . ab2)) <> {} by A17;
( (export F2) . a1 = F2 ?- a1 & (export F1) . a1 = F1 ?- a1 ) by Th18;
then A33: t . a1 = [[G1,H1],t1] by A7, A26;
A34: Hom ((G1 . b1),(H1 . b1)) <> {} by A27, ISOCAT_1:25;
( (export F1) . a2 = F1 ?- a2 & (export F2) . a2 = F2 ?- a2 ) by Th18;
then A35: t . a2 = [[G2,H2],t2] by A7, A22;
A36: Hom (((export F1) . a2),((export F2) . a2)) <> {} by A1, ISOCAT_1:25;
A37: Hom (((export F1) . a1),((export F2) . a1)) <> {} by A1, ISOCAT_1:25;
let f be Morphism of ab1,ab2; :: thesis: (u . ab2) * (F1 /. f) = (F2 /. f) * (u . ab1)
consider g being Morphism of A, h being Morphism of B such that
A38: f = [g,h] by DOMAIN_1:1;
reconsider g = g as Morphism of a1,a2 by A19, A25, A21, A38, Th10;
A39: Hom (a1,a2) <> {} by A19, A25, A21, Th9;
then A40: ( dom g = a1 & cod g = a2 ) by CAT_1:5;
reconsider h = h as Morphism of b1,b2 by A19, A25, A21, A38, Th10;
reconsider g9 = g as Morphism of A ;
reconsider h9 = h as Morphism of B ;
reconsider f9 = f as Morphism of [:A,B:] ;
A41: dom (id b2) = b2 ;
Hom (a1,a1) <> {} ;
then A42: g9 (*) (id a1) = g * (id a1) by A39, CAT_1:def 13
.= g by A39, CAT_1:29 ;
A43: dom g = a1 by A39, CAT_1:5;
A44: Hom (((export F2) . a1),((export F2) . a2)) <> {} by A39, CAT_1:84;
reconsider e1 = (export F1) /. g, e2 = (export F2) /. g as Morphism of (Functors (B,C)) ;
A45: Hom ((F1 . ab1),(F2 . ab1)) <> {} by A17;
A46: Hom (b1,b2) <> {} by A19, A25, A21, Th9;
then A47: Hom ((G1 . b1),(G1 . b2)) <> {} by CAT_1:84;
A48: [(F1 ?- a1),(F2 ?- a1)] = [G1,H1] by A26, XTUPLE_0:1;
then A49: F2 ?- a1 = H1 by XTUPLE_0:1;
then A50: H1 /. h = (F2 ?- a1) /. h by A46, CAT_3:def 10
.= F2 . ((id a1),h) by CAT_2:36 ;
A51: [(F1 ?- a2),(F2 ?- a2)] = [G2,H2] by A22, XTUPLE_0:1;
then A52: F2 ?- a2 = H2 by XTUPLE_0:1;
then A53: Hom ((H1 . b2),(H2 . b2)) <> {} by A49, A40, Th14, ISOCAT_1:25;
A54: F1 ?- a2 = G2 by A51, XTUPLE_0:1;
then reconsider v1 = F1 ?- g as natural_transformation of G1,G2 by A48, A40, XTUPLE_0:1;
A55: Hom (((export F1) . a1),((export F1) . a2)) <> {} by A39, CAT_1:84;
( cod (id a1) = a1 & cod h = b2 ) by A46, CAT_1:5;
then A56: cod [(id a1),h] = [a1,b2] by CAT_2:28
.= dom [g,(id b2)] by A43, A41, CAT_2:28 ;
reconsider v2 = F2 ?- g as natural_transformation of H1,H2 by A48, A52, A40, XTUPLE_0:1;
A57: (export F2) . g9 = [[H1,H2],v2] by A49, A52, A40, Def4;
A58: id b2 = (IdMap B) . b2 by ISOCAT_1:def 12;
A59: H1 is_naturally_transformable_to H2 by A49, A52, A40, Th14;
then H1 is_transformable_to H2 ;
then A60: v2 . b2 = ((curry (F2,g)) * (IdMap B)) . b2 by NATTRA_1:def 5
.= (curry (F2,g)) . ((IdMap B) . b2) by FUNCT_2:15
.= F2 . (g,(id b2)) by A58, FUNCT_5:69 ;
A61: F1 ?- a1 = G1 by A48, XTUPLE_0:1;
then A62: G1 /. h = (F1 ?- a1) /. h by A46, CAT_3:def 10
.= F1 . ((id a1),h) by CAT_2:36 ;
(export F1) . g9 = [[G1,G2],v1] by A61, A54, A40, Def4;
then [[G1,H2],(t2 `*` v1)] = (t . a2) (*) ((export F1) . g9) by A35, NATTRA_1:36
.= (t . a2) (*) e1 by A39, CAT_3:def 10
.= (t . a2) * ((export F1) /. g) by A55, A36, CAT_1:def 13
.= ((export F2) /. g) * (t . a1) by A1, A39, NATTRA_1:def 8
.= e2 (*) (t . a1) by A44, A37, CAT_1:def 13
.= ((export F2) . g9) (*) (t . a1) by A39, CAT_3:def 10
.= [[G1,H2],(v2 `*` t1)] by A57, A33, NATTRA_1:36 ;
then A63: t2 `*` v1 = v2 `*` t1 by XTUPLE_0:1;
A64: id b2 = (IdMap B) . b2 by ISOCAT_1:def 12;
A65: G1 is_naturally_transformable_to G2 by A61, A54, A40, Th14;
then G1 is_transformable_to G2 ;
then A66: v1 . b2 = ((curry (F1,g)) * (IdMap B)) . b2 by NATTRA_1:def 5
.= (curry (F1,g)) . ((IdMap B) . b2) by FUNCT_2:15
.= F1 . (g,(id b2)) by A64, FUNCT_5:69 ;
A67: u . ab2 = u9 . (a2,b2) by A17, A21, NATTRA_1:def 5
.= (t9 . a2) . b2 by Th2
.= t2 . b2 by A24, NATTRA_1:def 5 ;
A68: Hom ((G2 . b2),(H2 . b2)) <> {} by A23, ISOCAT_1:25;
Hom (b2,b2) <> {} ;
then (id b2) (*) h9 = (id b2) * h by A46, CAT_1:def 13
.= h by A46, CAT_1:28 ;
then A69: f = [g,(id b2)] (*) [(id a1),h] by A38, A42, A56, CAT_2:30;
A70: Hom ((H1 . b1),(H1 . b2)) <> {} by A46, CAT_1:84;
then A71: Hom ((H1 . b1),(H2 . b2)) <> {} by A53, CAT_1:24;
A72: F2 /. f = F2 /. f9 by A19, CAT_3:def 10
.= (v2 . b2) (*) (H1 /. h) by A56, A69, A60, A50, CAT_1:64
.= (v2 . b2) * (H1 /. h) by A53, A70, CAT_1:def 13 ;
A73: Hom ((G1 . b2),(G2 . b2)) <> {} by A61, A54, A40, Th14, ISOCAT_1:25;
then A74: Hom ((G1 . b1),(G2 . b2)) <> {} by A47, CAT_1:24;
F1 /. f = F1 /. f9 by A19, CAT_3:def 10
.= (v1 . b2) (*) (G1 /. h) by A56, A69, A66, A62, CAT_1:64
.= (v1 . b2) * (G1 /. h) by A73, A47, CAT_1:def 13 ;
hence (u . ab2) * (F1 /. f) = (t2 . b2) (*) ((v1 . b2) * (G1 /. h)) by A31, A32, A67, CAT_1:def 13
.= (t2 . b2) * ((v1 . b2) * (G1 /. h)) by A68, A74, CAT_1:def 13
.= ((t2 . b2) * (v1 . b2)) * (G1 /. h) by A68, A73, A47, CAT_1:25
.= ((v2 `*` t1) . b2) * (G1 /. h) by A23, A65, A63, NATTRA_1:25
.= ((v2 . b2) * (t1 . b2)) * (G1 /. h) by A27, A59, NATTRA_1:25
.= (v2 . b2) * ((t1 . b2) * (G1 /. h)) by A47, A53, A30, CAT_1:25
.= (v2 . b2) * ((H1 /. h) * (t1 . b1)) by A27, A46, NATTRA_1:def 8
.= ((v2 . b2) * (H1 /. h)) * (t1 . b1) by A53, A70, A34, CAT_1:25
.= (F2 /. f) (*) (u . ab1) by A34, A71, A29, A72, CAT_1:def 13
.= (F2 /. f) * (u . ab1) by A45, A20, CAT_1:def 13 ;
:: thesis: verum

end;

hence A75: F1 is_naturally_transformable_to F2 by A17; :: thesis: ex u being natural_transformation of F1,F2 st t = export u
then reconsider u = u as natural_transformation of F1,F2 by A18, NATTRA_1:def 8;
take u ; :: thesis: t = export u

now :: thesis: for s being Function of [: the carrier of A, the carrier of B:], the carrier' of C st u = s holds
for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]

let s be Function of [: the carrier of A, the carrier of B:], the carrier' of C; :: thesis: ( u = s implies for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] )
assume A76: u = s ; :: thesis: for a being Object of A holds t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
let a be Object of A; :: thesis: t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)]
t9 = curry u9 by Th1;
hence t . a = [[((export F1) . a),((export F2) . a)],((curry s) . a)] by A7, A76; :: thesis: verum

end;

hence t = export u by A75, Def5; :: thesis: verum