defpred S₁[ object , object ] 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 = [[(export F1),(export F2)],(export t)];

let F19, F29 be Functor of [:A,B:],C; :: thesis:
let t9 be natural_transformation of F19,F29; :: thesis:
assume A4: o = [[F19,F29],t9] ; :: thesis:
then [F1,F2] = [F19,F29] by A2, XTUPLE_0:1;
then ( F1 = F19 & F2 = F29 ) by XTUPLE_0:1;
hence m = [[(export F19),(export F29)],(export t9)] by A2, A4, XTUPLE_0:1; :: thesis:

end;

consider FF being Function of the carrier' of (Functors ([:A,B:],C)), the carrier' of (Functors (A,(Functors (B,C)))) such that
A5: for o being object st o in the carrier' of (Functors ([:A,B:],C)) holds
S₁[o,FF . o] from FUNCT_2:sch 1(A1);
FF is Functor of Functors ([:A,B:],C), Functors (A,(Functors (B,C)))

thus for c being Object of (Functors ([:A,B:],C)) ex d being Object of (Functors (A,(Functors (B,C)))) st FF . (id c) = id d :: according to ISOCAT_1:def 1 :: thesis:

let c be Object of (Functors ([:A,B:],C)); :: thesis:
reconsider F = c as Functor of [:A,B:],C by Th5;
reconsider d = export F as Object of (Functors (A,(Functors (B,C)))) by Th5;
take d ; :: thesis:
A6: id (export F) = export (id F) by Th22;
id c = [[F,F],(id F)] by NATTRA_1:def 17;
hence FF . (id c) = [[(export F),(export F)],(export (id F))] by A5
.= id d by A6, NATTRA_1:def 17 ;
:: thesis:

end;

thus for f being Morphism of (Functors ([:A,B:],C)) holds
( FF . (id (dom f)) = id (dom (FF . f)) & FF . (id (cod f)) = id (cod (FF . f)) ) :: thesis:

let f be Morphism of (Functors ([:A,B:],C)); :: thesis:
consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that
F1 is_naturally_transformable_to F2 and
A7: dom f = F1 and
A8: cod f = F2 and
A9: f = [[F1,F2],t] by Th6;
A10: FF . f = [[(export F1),(export F2)],(export t)] by A5, A9;
then A11: dom (FF . f) = export F1 by NATTRA_1:33;
id (dom f) = [[F1,F1],(id F1)] by A7, NATTRA_1:def 17;
hence FF . (id (dom f)) = [[(export F1),(export F1)],(export (id F1))] by A5
.= [[(export F1),(export F1)],(id (export F1))] by Th22
.= id (dom (FF . f)) by A11, NATTRA_1:def 17 ;
:: thesis:
A12: cod (FF . f) = export F2 by A10, NATTRA_1:33;
id (cod f) = [[F2,F2],(id F2)] by A8, NATTRA_1:def 17;
hence FF . (id (cod f)) = [[(export F2),(export F2)],(export (id F2))] by A5
.= [[(export F2),(export F2)],(id (export F2))] by Th22
.= id (cod (FF . f)) by A12, NATTRA_1:def 17 ;
:: thesis:

end;

let f, g be Morphism of (Functors ([:A,B:],C)); :: thesis:
consider F1, F2 being Functor of [:A,B:],C, t being natural_transformation of F1,F2 such that
A13: F1 is_naturally_transformable_to F2 and
dom f = F1 and
A14: cod f = F2 and
A15: f = [[F1,F2],t] by Th6;
A16: FF . f = [[(export F1),(export F2)],(export t)] by A5, A15;
consider G1, G2 being Functor of [:A,B:],C, u being natural_transformation of G1,G2 such that
A17: G1 is_naturally_transformable_to G2 and
A18: dom g = G1 and
cod g = G2 and
A19: g = [[G1,G2],u] by Th6;
assume A20: dom g = cod f ; :: thesis:
then reconsider u = u as natural_transformation of F2,G2 by A14, A18;
g (*) f = [[F1,G2],(u `*` t)] by A14, A15, A18, A19, A20, NATTRA_1:36;
then A21: FF . (g (*) f) = [[(export F1),(export G2)],(export (u `*` t))] by A5;
( FF . g = [[(export F2),(export G2)],(export u)] & (export u) `*` (export t) = export (u `*` t) ) by A5, A13, A14, A17, A18, A19, A20, Th23;
hence FF . (g (*) f) = (FF . g) (*) (FF . f) by A16, A21, NATTRA_1:36; :: thesis:

end;