for n being non empty Nat
for xv, yv being Element of (n -VectSp_over F_Real)
for xt, yt being Element of (TOP-REAL n) st xv = xt & yv = yt holds
xv - yv = xt - yt