defpred S_{1}[ Object of A, object ] means $2 = (t2 ! $1) * (t1 ! $1);

A2: for a being Element of A ex j being object st S_{1}[a,j]
;

consider t being ManySortedSet of the carrier of A such that

A3: for a being Element of A holds S_{1}[a,t . a]
from PBOOLE:sch 6(A2);

A4: F is_transformable_to F2 by A1, Th2;

for a being Object of A holds t . a is Morphism of (F . a),(F2 . a)

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

let a be Element of A; :: thesis: t9 ! a = (t2 ! a) * (t1 ! a)

S_{1}[a,t . a]
by A3;

hence t9 ! a = (t2 ! a) * (t1 ! a) by A4, Def4; :: thesis: verum

A2: for a being Element of A ex j being object st S

consider t being ManySortedSet of the carrier of A such that

A3: for a being Element of A holds S

A4: F is_transformable_to F2 by A1, Th2;

for a being Object of A holds t . a is Morphism of (F . a),(F2 . a)

proof

then reconsider t9 = t as transformation of F,F2 by A4, Def2;
let o be Element of A; :: thesis: t . o is Morphism of (F . o),(F2 . o)

S_{1}[o,t . o]
by A3;

hence t . o is Morphism of (F . o),(F2 . o) ; :: thesis: verum

end;S

hence t . o is Morphism of (F . o),(F2 . o) ; :: thesis: verum

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

let a be Element of A; :: thesis: t9 ! a = (t2 ! a) * (t1 ! a)

S

hence t9 ! a = (t2 ! a) * (t1 ! a) by A4, Def4; :: thesis: verum