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

now

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

end;

hence t = t' by A1, A2, Lm3, Th20; :: thesis: verum