deffunc H_{1}( 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_{1}(a)
from FUNCT_2:sch 4();

A4: for a being Object of A holds t . a is Morphism of F . a,F2 . a

then reconsider t9 = t as transformation of F,F2 by A4, Def2;

take t9 ; :: thesis: for a being Object of A holds t9 . a = (t2 . a) * (t1 . a)

let a be Object of A; :: thesis: t9 . a = (t2 . a) * (t1 . a)

thus t9 . a = t . a by A1, A2, Def4, Th14

.= (t2 . a) * (t1 . a) by A3 ; :: thesis: verum

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

A4: for a being Object of A holds t . a is Morphism of F . a,F2 . a

proof

F is_transformable_to F2
by A1, A2, Th14;
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;t . a = (t2 . a) * (t1 . a) by A3;

hence t . a is Morphism of F . a,F2 . a ; :: thesis: verum

then reconsider t9 = t as transformation of F,F2 by A4, Def2;

take t9 ; :: thesis: for a being Object of A holds t9 . a = (t2 . a) * (t1 . a)

let a be Object of A; :: thesis: t9 . a = (t2 . a) * (t1 . a)

thus t9 . a = t . a by A1, A2, Def4, Th14

.= (t2 . a) * (t1 . a) by A3 ; :: thesis: verum