let n be Element of NAT ; :: thesis: for r being real number
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
Proj (r * p),i = r * (Proj p,i)
let r be real number ; :: thesis: for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
Proj (r * p),i = r * (Proj p,i)
let p be Point of (TOP-REAL n); :: thesis: for i being Element of NAT st i in Seg n holds
Proj (r * p),i = r * (Proj p,i)
let i be Element of NAT ; :: thesis: ( i in Seg n implies Proj (r * p),i = r * (Proj p,i) )
assume A1: i in Seg n ; :: thesis: Proj (r * p),i = r * (Proj p,i)
reconsider w1 = p as Element of REAL n by EUCLID:25;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
reconsider w = r * p as Element of REAL n by EUCLID:25;
i in Seg (len w1) by A1, FINSEQ_1:def 18;
then A2: i in dom w1 by FINSEQ_1:def 3;
A3: Proj p,i = w1 /. i by Def1
.= w3 . i by A2, PARTFUN1:def 8 ;
len w = n by FINSEQ_1:def 18;
then A4: i in dom w by A1, FINSEQ_1:def 3;
Proj (r * p),i = w /. i by Def1
.= w . i by A4, PARTFUN1:def 8
.= (r * w3) . i by A3, EUCLID:69
.= r * (w3 . i) by A3, RVSUM_1:67
.= r * (Proj p,i) by A3, RVSUM_1:67 ;
hence Proj (r * p),i = r * (Proj p,i) ; :: thesis: verum