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

A7: F is_transformable_to F2 by A1, Th2;

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

A7: F is_transformable_to F2 by A1, Th2;

now :: thesis: for a being object st a in the carrier of A holds

it1 . a = it2 . a

hence
it1 = it2
by PBOOLE:3; :: thesis: verumit1 . 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 = it1 ! o by A7, Def4

.= (t2 ! o) * (t1 ! o) by A5

.= it2 ! o by A6

.= it2 . a by A7, Def4 ; :: thesis: verum

end;assume a in the carrier of A ; :: thesis: it1 . a = it2 . a

then reconsider o = a as Object of A ;

thus it1 . a = it1 ! o by A7, Def4

.= (t2 ! o) * (t1 ! o) by A5

.= it2 ! o by A6

.= it2 . a by A7, Def4 ; :: thesis: verum