let it1, it2 be transformation of F,F2; :: thesis: ( ( for a being object of A holds it1 ! a = (t2 ! a) * (t1 ! a) ) & ( for a being object of A holds it2 ! a = (t2 ! a) * (t1 ! a) ) implies it1 = it2 )
assume that
A9: for a being object of A holds it1 ! a = (t2 ! a) * (t1 ! a) and
A10: for a being object of A holds it2 ! a = (t2 ! a) * (t1 ! a) ; :: thesis: it1 = it2
A11: F is_transformable_to F2 by A1, A2, Th4;

now

let a be set ; :: thesis: ( a in the carrier of A implies it1 . a = it2 . a )
assume a in the carrier of A ; :: thesis: it1 . a = it2 . a
then reconsider o = a as object of A ;
thus it1 . a = it1 ! o by A11, Def4
.= (t2 ! o) * (t1 ! o) by A9
.= it2 ! o by A10
.= it2 . a by A11, Def4 ; :: thesis: verum

end;

hence it1 = it2 by PBOOLE:3; :: thesis: verum