defpred S₁[ set , set ] means for F1, F2 being Functor of A,[:B,C:]
for t being natural_transformation of F1,F2 st $1 = [[F1,F2],t] holds
$2 = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]];

A1: now :: thesis: for f being Morphism of (Functors (A,[:B,C:])) ex g being Element of the carrier' of [:(Functors (A,B)),(Functors (A,C)):] st S₁[f,g]

let f be Morphism of (Functors (A,[:B,C:])); :: thesis: ex g being Element of the carrier' of [:(Functors (A,B)),(Functors (A,C)):] st S₁[f,g]
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A2: F1 is_naturally_transformable_to F2 and
dom f = F1 and
cod f = F2 and
A3: f = [[F1,F2],s] by Th6;
( the carrier' of (Functors (A,C)) = NatTrans (A,C) & Pr2 F1 is_naturally_transformable_to Pr2 F2 ) by A2, ISOCAT_1:22, NATTRA_1:def 17;
then reconsider PPr2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by NATTRA_1:32;
( the carrier' of (Functors (A,B)) = NatTrans (A,B) & Pr1 F1 is_naturally_transformable_to Pr1 F2 ) by A2, ISOCAT_1:22, NATTRA_1:def 17;
then reconsider PPr1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by NATTRA_1:32;
take g = [PPr1,PPr2]; :: thesis: S₁[f,g]
thus S₁[f,g] :: thesis: verum

proof

let G1, G2 be Functor of A,[:B,C:]; :: thesis: for t being natural_transformation of G1,G2 st f = [[G1,G2],t] holds
g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]]
let t be natural_transformation of G1,G2; :: thesis: ( f = [[G1,G2],t] implies g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] )
assume A4: f = [[G1,G2],t] ; :: thesis: g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]]
then [G1,G2] = [F1,F2] by A3, XTUPLE_0:1;
then A5: ( G1 = F1 & G2 = F2 ) by XTUPLE_0:1;
t = s by A3, A4, XTUPLE_0:1;
hence g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] by A5; :: thesis: verum

end;

end;

consider IT being Function of the carrier' of (Functors (A,[:B,C:])), the carrier' of [:(Functors (A,B)),(Functors (A,C)):] such that
A6: for f being Morphism of (Functors (A,[:B,C:])) holds S₁[f,IT . f] from FUNCT_2:sch 3(A1);
IT is Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):]

proof

thus for c being Object of (Functors (A,[:B,C:])) ex d being Object of [:(Functors (A,B)),(Functors (A,C)):] st IT . (id c) = id d :: according to ISOCAT_1:def 1 :: thesis: ( ( for b₁ being Element of the carrier' of (Functors (A,[:B,C:])) holds
( IT . (id (dom b₁)) = id (dom (IT . b₁)) & IT . (id (cod b₁)) = id (cod (IT . b₁)) ) ) & ( for b₁, b₂ being Element of the carrier' of (Functors (A,[:B,C:])) holds
( not dom b₂ = cod b₁ or IT . (b₂ (*) b₁) = (IT . b₂) (*) (IT . b₁) ) ) )

proof

let c be Object of (Functors (A,[:B,C:])); :: thesis: ex d being Object of [:(Functors (A,B)),(Functors (A,C)):] st IT . (id c) = id d
reconsider F = c as Functor of A,[:B,C:] by Th5;
reconsider d2 = Pr2 F as Object of (Functors (A,C)) by Th5;
reconsider d1 = Pr1 F as Object of (Functors (A,B)) by Th5;
take [d1,d2] ; :: thesis: IT . (id c) = id [d1,d2]
Pr1 (id F) = id (Pr1 F) by ISOCAT_1:33;
then A7: id d1 = [[(Pr1 F),(Pr1 F)],(Pr1 (id F))] by NATTRA_1:def 17;
Pr2 (id F) = id (Pr2 F) by ISOCAT_1:33;
then A8: id d2 = [[(Pr2 F),(Pr2 F)],(Pr2 (id F))] by NATTRA_1:def 17;
id c = [[F,F],(id F)] by NATTRA_1:def 17;
hence IT . (id c) = [(id d1),(id d2)] by A6, A7, A8
.= id [d1,d2] by CAT_2:31 ;
:: thesis: verum

end;

A9: the carrier' of (Functors (A,C)) = NatTrans (A,C) by NATTRA_1:def 17;
A10: the carrier' of (Functors (A,B)) = NatTrans (A,B) by NATTRA_1:def 17;
thus for f being Morphism of (Functors (A,[:B,C:])) holds
( IT . (id (dom f)) = id (dom (IT . f)) & IT . (id (cod f)) = id (cod (IT . f)) ) :: thesis: for b₁, b₂ being Element of the carrier' of (Functors (A,[:B,C:])) holds
( not dom b₂ = cod b₁ or IT . (b₂ (*) b₁) = (IT . b₂) (*) (IT . b₁) )

proof

let f be Morphism of (Functors (A,[:B,C:])); :: thesis: ( IT . (id (dom f)) = id (dom (IT . f)) & IT . (id (cod f)) = id (cod (IT . f)) )
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A11: F1 is_naturally_transformable_to F2 and
A12: dom f = F1 and
A13: cod f = F2 and
A14: f = [[F1,F2],s] by Th6;
Pr1 F1 is_naturally_transformable_to Pr1 F2 by A11, ISOCAT_1:22;
then reconsider f1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by A10, NATTRA_1:32;
( dom f1 = Pr1 F1 & Pr1 (id F1) = id (Pr1 F1) ) by ISOCAT_1:33, NATTRA_1:33;
then A15: id (dom f1) = [[(Pr1 F1),(Pr1 F1)],(Pr1 (id F1))] by NATTRA_1:def 17;
Pr2 F1 is_naturally_transformable_to Pr2 F2 by A11, ISOCAT_1:22;
then reconsider f2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by A9, NATTRA_1:32;
( dom f2 = Pr2 F1 & Pr2 (id F1) = id (Pr2 F1) ) by ISOCAT_1:33, NATTRA_1:33;
then A16: id (dom f2) = [[(Pr2 F1),(Pr2 F1)],(Pr2 (id F1))] by NATTRA_1:def 17;
id (dom f) = [[F1,F1],(id F1)] by A12, NATTRA_1:def 17;
hence IT . (id (dom f)) = [(id (dom f1)),(id (dom f2))] by A6, A15, A16
.= id [(dom f1),(dom f2)] by CAT_2:31
.= id (dom [f1,f2]) by CAT_2:28
.= id (dom (IT . f)) by A6, A14 ;
:: thesis: IT . (id (cod f)) = id (cod (IT . f))
( cod f1 = Pr1 F2 & Pr1 (id F2) = id (Pr1 F2) ) by ISOCAT_1:33, NATTRA_1:33;
then A17: id (cod f1) = [[(Pr1 F2),(Pr1 F2)],(Pr1 (id F2))] by NATTRA_1:def 17;
( cod f2 = Pr2 F2 & Pr2 (id F2) = id (Pr2 F2) ) by ISOCAT_1:33, NATTRA_1:33;
then A18: id (cod f2) = [[(Pr2 F2),(Pr2 F2)],(Pr2 (id F2))] by NATTRA_1:def 17;
id (cod f) = [[F2,F2],(id F2)] by A13, NATTRA_1:def 17;
hence IT . (id (cod f)) = [(id (cod f1)),(id (cod f2))] by A6, A17, A18
.= id [(cod f1),(cod f2)] by CAT_2:31
.= id (cod [f1,f2]) by CAT_2:28
.= id (cod (IT . f)) by A6, A14 ;
:: thesis: verum

end;

let f, g be Morphism of (Functors (A,[:B,C:])); :: thesis: ( not dom g = cod f or IT . (g (*) f) = (IT . g) (*) (IT . f) )
assume A19: dom g = cod f ; :: thesis: IT . (g (*) f) = (IT . g) (*) (IT . f)
consider F1, F2 being Functor of A,[:B,C:], s being natural_transformation of F1,F2 such that
A20: F1 is_naturally_transformable_to F2 and
dom f = F1 and
A21: cod f = F2 and
A22: f = [[F1,F2],s] by Th6;
consider G1, G2 being Functor of A,[:B,C:], t being natural_transformation of G1,G2 such that
A23: G1 is_naturally_transformable_to G2 and
A24: dom g = G1 and
cod g = G2 and
A25: g = [[G1,G2],t] by Th6;
reconsider t = t as natural_transformation of F2,G2 by A19, A21, A24;
A26: g (*) f = [[F1,G2],(t `*` s)] by A19, A21, A22, A24, A25, NATTRA_1:36;
A27: Pr2 F1 is_naturally_transformable_to Pr2 F2 by A20, ISOCAT_1:22;
Pr2 F2 is_naturally_transformable_to Pr2 G2 by A19, A21, A23, A24, ISOCAT_1:22;
then reconsider g2 = [[(Pr2 F2),(Pr2 G2)],(Pr2 t)], f2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by A9, A27, NATTRA_1:32;
A28: g2 (*) f2 = [[(Pr2 F1),(Pr2 G2)],((Pr2 t) `*` (Pr2 s))] by NATTRA_1:36
.= [[(Pr2 F1),(Pr2 G2)],(Pr2 (t `*` s))] by A19, A20, A21, A23, A24, ISOCAT_1:27 ;
A29: dom g2 = Pr2 F2 by NATTRA_1:33
.= cod f2 by NATTRA_1:33 ;
A30: Pr1 F1 is_naturally_transformable_to Pr1 F2 by A20, ISOCAT_1:22;
Pr1 F2 is_naturally_transformable_to Pr1 G2 by A19, A21, A23, A24, ISOCAT_1:22;
then reconsider g1 = [[(Pr1 F2),(Pr1 G2)],(Pr1 t)], f1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by A10, A30, NATTRA_1:32;
A31: dom g1 = Pr1 F2 by NATTRA_1:33
.= cod f1 by NATTRA_1:33 ;
A32: IT . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] by A6, A22;
g1 (*) f1 = [[(Pr1 F1),(Pr1 G2)],((Pr1 t) `*` (Pr1 s))] by NATTRA_1:36
.= [[(Pr1 F1),(Pr1 G2)],(Pr1 (t `*` s))] by A19, A20, A21, A23, A24, ISOCAT_1:27 ;
hence IT . (g (*) f) = [(g1 (*) f1),(g2 (*) f2)] by A6, A28, A26
.= [g1,g2] (*) [f1,f2] by A31, A29, CAT_2:29
.= (IT . g) (*) (IT . f) by A6, A19, A21, A24, A25, A32 ;
:: thesis: verum

end;

then reconsider IT = IT as Functor of Functors (A,[:B,C:]),[:(Functors (A,B)),(Functors (A,C)):] ;
take IT ; :: thesis: for F1, F2 being Functor of A,[:B,C:] st F1 is_naturally_transformable_to F2 holds
for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
let F1, F2 be Functor of A,[:B,C:]; :: thesis: ( F1 is_naturally_transformable_to F2 implies for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] )
assume A33: F1 is_naturally_transformable_to F2 ; :: thesis: for t being natural_transformation of F1,F2 holds IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
let t be natural_transformation of F1,F2; :: thesis: IT . [[F1,F2],t] = [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]]
set f = [[F1,F2],t];
[[F1,F2],t] in NatTrans (A,[:B,C:]) by A33, NATTRA_1:32;
then reconsider f = [[F1,F2],t] as Morphism of (Functors (A,[:B,C:])) by NATTRA_1:def 17;
thus IT . [[F1,F2],t] = IT . f
.= [[[(Pr1 F1),(Pr1 F2)],(Pr1 t)],[[(Pr2 F1),(Pr2 F2)],(Pr2 t)]] by A6 ; :: thesis: verum