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

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

hence
it1 = it2
; :: thesis: verumlet 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;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