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
reconsider x1 = x as Real by XREAL_0:def 1;
let r be real-valued Function; :: thesis: ( p = r implies x * p = x (#) r )
assume A1: p = r ; :: thesis: x * p = x (#) r
reconsider s = r as Element of REAL n by A1, EUCLID:22;
REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;
then reconsider f = s as Element of Funcs ((Seg n),REAL) ;
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 EUCLID:def 8;
then XX: the Mult of (TOP-REAL n) = the Mult of RLSStruct(# (Funcs ((Seg n),REAL)),(RealFuncZero (Seg n)),(RealFuncAdd (Seg n)),(RealFuncExtMult (Seg n)) #) by FUNCSDOM:def 6
.= RealFuncExtMult (Seg n) ;
thus x * p = (RealFuncExtMult (Seg n)) . (x,p) by XX
.= multreal [;] (x1,f) by A1, FUNCSDOM:def 3
.= multreal [;] (x,((id REAL) * f)) by PARTFUN1:7
.= (multreal [;] (x,(id REAL))) * f by FUNCOP_1:34
.= (x multreal) * s by RVSUM_1:def 3
.= x * s by RVSUM_1:def 7
.= x (#) r ; :: thesis: verum