reconsider t = <:t1,t2:> as Function of the carrier of A, the carrier' of [:B,C:] ;
t is transformation of <:F1,F2:>,<:G1,G2:>

proof

thus <:F1,F2:> is_transformable_to <:G1,G2:> by A1, Th34; :: according to NATTRA_1:def 3 :: thesis: for b₁ being Element of the carrier of A holds t . b₁ is Morphism of <:F1,F2:> . b₁,<:G1,G2:> . b₁
let a be Object of A; :: thesis: t . a is Morphism of <:F1,F2:> . a,<:G1,G2:> . a
t . a in Hom ((<:F1,F2:> . a),(<:G1,G2:> . a)) by A1, Lm3;
hence t . a is Morphism of <:F1,F2:> . a,<:G1,G2:> . a by CAT_1:def 5; :: thesis: verum

end;

hence <:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:> ; :: thesis: verum