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

now :: thesis: for a being Object of A holds it1 . a = it2 . a

let a be Object of A; :: thesis: it1 . a = it2 . a
thus it1 . a = id (F . a) by A2
.= it2 . a by A3 ; :: thesis: verum

end;

hence it1 = it2 ; :: thesis: verum