deffunc H₁( Object of A) -> Morphism of F2 . $1,F1 . $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: now :: thesis: for a being Object of A holds t . a is Morphism of F2 . a,F1 . a

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

end;

F2 is_transformable_to F1 by A1, A2, Lm3;
then reconsider t = t as transformation of F2,F1 by A4, Def2;
take t ; :: thesis: for a being Object of A holds t . a = (t1 . a) "
let a be Object of A; :: thesis: t . a = (t1 . a) "
thus t . a = t . a by A1, A2, Def4, Lm3
.= (t1 . a) " by A3 ; :: thesis: verum