let n be Element of NAT ; :: thesis: for r being Real
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(r * p) /. i = r * (p /. i)
let r be Real; :: thesis: for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(r * p) /. i = r * (p /. i)
let p be Point of (TOP-REAL n); :: thesis: for i being Element of NAT st i in Seg n holds
(r * p) /. i = r * (p /. i)
let i be Element of NAT ; :: thesis: ( i in Seg n implies (r * p) /. i = r * (p /. i) )
reconsider w1 = p as Element of REAL n by EUCLID:22;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
reconsider w = r * p as Element of REAL n by EUCLID:22;
assume A1: i in Seg n ; :: thesis: (r * p) /. i = r * (p /. i)
then i in Seg (len w1) by CARD_1:def 7;
then A2: i in dom w1 by FINSEQ_1:def 3;
len w = n by CARD_1:def 7;
then A3: i in dom w by A1, FINSEQ_1:def 3;
A4: p /. i = w3 . i by A2, PARTFUN1:def 6;
(r * p) /. i = w . i by A3, PARTFUN1:def 6
.= (r * w3) . i
.= r * (p /. i) by A4, RVSUM_1:45 ;
hence (r * p) /. i = r * (p /. i) ; :: thesis: verum