theorem :: REAL_NS2:56

for n being non empty Nat
for af being Element of F_Real
for at being Real
for xv being Element of (n -VectSp_over F_Real)
for xt being Element of (TOP-REAL n) st af = at & xv = xt holds
af * xv = at * xt by Th54;