let n be non empty Nat; :: thesis: 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
let xv, yv be Element of (n -VectSp_over F_Real); :: thesis: for xt, yt being Element of (TOP-REAL n) st xv = xt & yv = yt holds
xv - yv = xt - yt
let xt, yt be Element of (TOP-REAL n); :: thesis: ( xv = xt & yv = yt implies xv - yv = xt - yt )
assume A1: ( xv = xt & yv = yt ) ; :: thesis: xv - yv = xt - yt
then - yv = - yt by Th57;
hence xv - yv = xt - yt by A1, Th54; :: thesis: verum