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
A3: for a being Object of A holds t . a = (t1 . a) " and
A4: 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 A3
.= t9 . a by A4 ; :: thesis: verum

end;

hence t = t9 by B1, B2, Lm3, Th19; :: thesis: verum