deffunc H₁( Object of A) -> Morphism of F . $1,F . $1 = id (F . $1);
consider t being Function of the carrier of A, the carrier' of B such that
A1: for a being Object of A holds t . a = H₁(a) from FUNCT_2:sch 4();
for a being Object of A holds t . a is Morphism of F . a,F . a

proof

let a be Object of A; :: thesis: t . a is Morphism of F . a,F . a
t . a = id (F . a) by A1;
hence t . a is Morphism of F . a,F . a ; :: thesis: verum

end;

then reconsider t = t as transformation of F,F by Def2;
take t ; :: thesis: for a being Object of A holds t . a = id (F . a)
let a be Object of A; :: thesis: t . a = id (F . a)
thus t . a = id (F . a) by A1; :: thesis: verum