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
A5: for a being Object of A holds it1 ! a = (t2 ! a) * (t1 ! a) and
A6: for a being Object of A holds it2 ! a = (t2 ! a) * (t1 ! a) ; :: thesis: it1 = it2
A7: F is_transformable_to F2 by A1, Th2;

now :: thesis: for a being object st a in the carrier of A holds
it1 . a = it2 . a

let a be object ; :: 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 A7, Def4
.= (t2 ! o) * (t1 ! o) by A5
.= it2 ! o by A6
.= it2 . a by A7, Def4 ; :: thesis: verum

end;

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