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;
NATTRA_1:def 3 for b1 being Element of the carrier of A holds t . b1 is Morphism of <:F1,F2:> . b1,<:G1,G2:> . b1
let a be
Object of
A;
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;
verum
end;
hence
<:t1,t2:> is transformation of <:F1,F2:>,<:G1,G2:>
; verum