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 :: 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 = it1 . a by A1, A2, Def4, Th14
.= (t2 . a) * (t1 . a) by A5
.= it2 . a by A6
.= it2 . a by A1, A2, Def4, Th14 ; :: thesis: verum
end;
hence it1 = it2 ; :: thesis: verum