let t, t9 be transformation of F2,F1; :: thesis: ( ( for a being Object of A holds t . a = (t1 . a) " ) & ( for a being Object of A holds t9 . a = (t1 . a) " ) implies t = t9 )
assume that
A5: for a being Object of A holds t . a = (t1 . a) " and
A6: for a being Object of A holds t9 . a = (t1 . a) " ; :: thesis: t = t9

now :: thesis: for a being Object of A holds t . a = t9 . a

let a be Object of A; :: thesis: t . a = t9 . a
thus t . a = (t1 . a) " by A5
.= t9 . a by A6 ; :: thesis: verum

end;

hence t = t9 by A1, A2, Lm3, Th15; :: thesis: verum