deffunc H₁( Object of A) -> Morphism of F . $1,F2 . $1 = (t2 . $1) * (t1 . $1);
consider t being Function of the carrier of A,the carrier' of B such that
A3: for a being Object of A holds t . a = H₁(a) from FUNCT_2:sch 4();
A4: F is_transformable_to F2 by A1, A2, Th19;
for a being Object of A holds t . a is Morphism of F . a,F2 . a

proof

let a be Object of A; :: thesis: t . a is Morphism of F . a,F2 . a
t . a = (t2 . a) * (t1 . a) by A3;
hence t . a is Morphism of F . a,F2 . a ; :: thesis: verum

end;

then reconsider t' = t as transformation of F,F2 by A4, Def3;
take t' ; :: thesis: for a being Object of A holds t' . a = (t2 . a) * (t1 . a)
let a be Object of A; :: thesis: t' . a = (t2 . a) * (t1 . a)
thus t' . a = t . a by A1, A2, Def5, Th19
.= (t2 . a) * (t1 . a) by A3 ; :: thesis: verum