let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for x being real number
for r being real-valued Function st p = r holds
x * p = x (#) r
let p be Point of (TOP-REAL n); :: thesis: for x being real number
for r being real-valued Function st p = r holds
x * p = x (#) r
let x be real number ; :: thesis: for r being real-valued Function st p = r holds
x * p = x (#) r
let r be real-valued Function; :: thesis: ( p = r implies x * p = x (#) r )
assume Z1: p = r ; :: thesis: x * p = x (#) r
X1: RLSStruct(# the carrier of (TOP-REAL n),the ZeroF of (TOP-REAL n),the addF of (TOP-REAL n),the Mult of (TOP-REAL n) #) = RealVectSpace (Seg n) by Def8;
reconsider s = r as Element of REAL n by Z1, Th25;
REAL n = Funcs (Seg n),REAL by FINSEQ_2:111;
then reconsider f = s as Function of (Seg n),REAL by FUNCT_2:121;
reconsider x1 = x as Real by XREAL_0:def 1;
thus x * p = multreal [;] x1,f by Z1, X1, FUNCSDOM:def 4
.= multreal [;] x,((id REAL ) * f) by PARTFUN1:37
.= x * s by FUNCOP_1:44
.= x (#) r ; :: thesis: verum