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

now

let a be Object of A; :: thesis: it1 . a = it2 . a
thus it1 . a = it1 . a by A1, A2, Def5, Th19
.= (t2 . a) * (t1 . a) by A5
.= it2 . a by A6
.= it2 . a by A1, A2, Def5, Th19 ; :: thesis: verum

end;

hence it1 = it2 by FUNCT_2:113; :: thesis: verum