theorem :: REAL_NS2:55

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 by Th54;