let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for x being Real
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
for r being real-valued Function st p = r holds
x * p = x (#) r
let x be Real; :: thesis: for r being real-valued Function st p = r holds
x * p = x (#) r
reconsider x1 = x as Real ;
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, Th19;
REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;
then reconsider f = s as Function of (Seg n),REAL by FUNCT_2:66;
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;
hence x * p = multreal [;] (x1,f) by A1, FUNCSDOM:def 3
.= multreal [;] (x,((id REAL) * f)) by PARTFUN1:7
.= x * s by FUNCOP_1:34
.= x (#) r ;
:: thesis: verum