let n, i be Element of NAT ; :: thesis: for y1 being Point of (REAL-NS n)
for r being Real holds (Proj i,n) . (r * y1) = r * ((Proj i,n) . y1)
let y1 be Point of (REAL-NS n); :: thesis: for r being Real holds (Proj i,n) . (r * y1) = r * ((Proj i,n) . y1)
let r be Real; :: thesis: (Proj i,n) . (r * y1) = r * ((Proj i,n) . y1)
reconsider yy1 = y1 as Element of REAL n by REAL_NS1:def 4;
reconsider y1i = yy1 . i as Element of REAL ;
(Proj i,n) . y1 = <*((proj i,n) . y1)*> by PDIFF_1:def 4;
then Q1: (Proj i,n) . y1 = <*y1i*> by PDIFF_1:def 1;
Q2: <*y1i*> is Element of REAL 1 by FINSEQ_2:118;
(Proj i,n) . (r * y1) = <*((proj i,n) . (r * y1))*> by PDIFF_1:def 4
.= <*((proj i,n) . (r * yy1))*> by REAL_NS1:3
.= <*((r * yy1) . i)*> by PDIFF_1:def 1
.= <*(r * (yy1 . i))*> by RVSUM_1:66
.= r * <*y1i*> by RVSUM_1:69 ;
hence (Proj i,n) . (r * y1) = r * ((Proj i,n) . y1) by Q1, Q2, REAL_NS1:3; :: thesis: verum