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

let f be Morphism of (Functors (A,[:B,C:])); :: thesis: ex g being Morphism 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 Th9;
( 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 A4: [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] is 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 [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] is Morphism of (Functors (A,B)) by NATTRA_1:32;
then reconsider g = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] as Morphism of [:(Functors (A,B)),(Functors (A,C)):] by A4, CAT_2:26;
take g = g; :: 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 A5: 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, ZFMISC_1:27;
then A6: ( G1 = F1 & G2 = F2 ) by ZFMISC_1:27;
t = s by A3, A5, ZFMISC_1:27;
hence g = [[[(Pr1 G1),(Pr1 G2)],(Pr1 t)],[[(Pr2 G1),(Pr2 G2)],(Pr2 t)]] by A6; :: 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
A7: 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 Th8;
reconsider d2 = Pr2 F as Object of (Functors (A,C)) by Th8;
reconsider d1 = Pr1 F as Object of (Functors (A,B)) by Th8;
take [d1,d2] ; :: thesis: IT . (id c) = id [d1,d2]
Pr1 (id F) = id (Pr1 F) by ISOCAT_1:33;
then A8: 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 A9: 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 A7, A8, A9
.= id [d1,d2] by CAT_2:31 ;
:: thesis: verum

end;

A10: the carrier' of (Functors (A,C)) = NatTrans (A,C) by NATTRA_1:def 17;
A11: 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
A12: F1 is_naturally_transformable_to F2 and
A13: dom f = F1 and
A14: cod f = F2 and
A15: f = [[F1,F2],s] by Th9;
Pr1 F1 is_naturally_transformable_to Pr1 F2 by A12, ISOCAT_1:22;
then reconsider f1 = [[(Pr1 F1),(Pr1 F2)],(Pr1 s)] as Morphism of (Functors (A,B)) by A11, NATTRA_1:32;
( dom f1 = Pr1 F1 & Pr1 (id F1) = id (Pr1 F1) ) by ISOCAT_1:33, NATTRA_1:33;
then A16: id (dom f1) = [[(Pr1 F1),(Pr1 F1)],(Pr1 (id F1))] by NATTRA_1:def 17;
Pr2 F1 is_naturally_transformable_to Pr2 F2 by A12, ISOCAT_1:22;
then reconsider f2 = [[(Pr2 F1),(Pr2 F2)],(Pr2 s)] as Morphism of (Functors (A,C)) by A10, NATTRA_1:32;
( dom f2 = Pr2 F1 & Pr2 (id F1) = id (Pr2 F1) ) by ISOCAT_1:33, NATTRA_1:33;
then A17: id (dom f2) = [[(Pr2 F1),(Pr2 F1)],(Pr2 (id F1))] by NATTRA_1:def 17;
id (dom f) = [[F1,F1],(id F1)] by A13, NATTRA_1:def 17;
hence IT . (id (dom f)) = [(id (dom f1)),(id (dom f2))] by A7, A16, A17
.= id [(dom f1),(dom f2)] by CAT_2:31
.= id (dom [f1,f2]) by CAT_2:28
.= id (dom (IT . f)) by A7, A15 ;
:: 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 A18: 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 A19: id (cod f2) = [[(Pr2 F2),(Pr2 F2)],(Pr2 (id F2))] by NATTRA_1:def 17;
id (cod f) = [[F2,F2],(id F2)] by A14, NATTRA_1:def 17;
hence IT . (id (cod f)) = [(id (cod f1)),(id (cod f2))] by A7, A18, A19
.= id [(cod f1),(cod f2)] by CAT_2:31
.= id (cod [f1,f2]) by CAT_2:28
.= id (cod (IT . f)) by A7, A15 ;
:: 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 A20: 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
A21: F1 is_naturally_transformable_to F2 and
dom f = F1 and
A22: cod f = F2 and
A23: f = [[F1,F2],s] by Th9;
consider G1, G2 being Functor of A,[:B,C:], t being natural_transformation of G1,G2 such that
A24: G1 is_naturally_transformable_to G2 and
A25: dom g = G1 and
cod g = G2 and
A26: g = [[G1,G2],t] by Th9;
reconsider t = t as natural_transformation of F2,G2 by A20, A22, A25;
A27: g * f = [[F1,G2],(t `*` s)] by A20, A22, A23, A25, A26, NATTRA_1:36;
A28: Pr2 F1 is_naturally_transformable_to Pr2 F2 by A21, ISOCAT_1:22;
Pr2 F2 is_naturally_transformable_to Pr2 G2 by A20, A22, A24, A25, 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 A10, A28, NATTRA_1:32;
A29: g2 * f2 = [[(Pr2 F1),(Pr2 G2)],((Pr2 t) `*` (Pr2 s))] by NATTRA_1:36
.= [[(Pr2 F1),(Pr2 G2)],(Pr2 (t `*` s))] by A20, A21, A22, A24, A25, ISOCAT_1:27 ;
A30: dom g2 = Pr2 F2 by NATTRA_1:33
.= cod f2 by NATTRA_1:33 ;
A31: Pr1 F1 is_naturally_transformable_to Pr1 F2 by A21, ISOCAT_1:22;
Pr1 F2 is_naturally_transformable_to Pr1 G2 by A20, A22, A24, A25, 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 A11, A31, NATTRA_1:32;
A32: dom g1 = Pr1 F2 by NATTRA_1:33
.= cod f1 by NATTRA_1:33 ;
A33: IT . f = [[[(Pr1 F1),(Pr1 F2)],(Pr1 s)],[[(Pr2 F1),(Pr2 F2)],(Pr2 s)]] by A7, A23;
g1 * f1 = [[(Pr1 F1),(Pr1 G2)],((Pr1 t) `*` (Pr1 s))] by NATTRA_1:36
.= [[(Pr1 F1),(Pr1 G2)],(Pr1 (t `*` s))] by A20, A21, A22, A24, A25, ISOCAT_1:27 ;
hence IT . (g * f) = [(g1 * f1),(g2 * f2)] by A7, A29, A27
.= [g1,g2] * [f1,f2] by A32, A30, CAT_2:29
.= (IT . g) * (IT . f) by A7, A20, A22, A25, A26, A33 ;
:: 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 A34: 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 A34, 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 A7 ; :: thesis: verum