let it1, it2 be transformation of F,F; :: thesis: ( ( for a being Object of A holds it1 . a = idm (F . a) ) & ( for a being Object of A holds it2 . a = idm (F . a) ) implies it1 = it2 )
assume that
A3: for a being Object of A holds it1 . a = idm (F . a) and
A4: for a being Object of A holds it2 . a = idm (F . a) ; :: thesis: it1 = it2

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 = idm (F . o) by A3
.= it2 . a by A4 ; :: thesis: verum

end;

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