let n be non zero Element of NAT ; :: thesis: for i being Nat
for y1 being Point of (REAL-NS n)
for r being Real holds (proj (i,n)) . (r * y1) = r * ((proj (i,n)) . y1)
let i be 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 by XREAL_0:def 1;
(proj (i,n)) . (r * y1) = (proj (i,n)) . (r * yy1) by REAL_NS1:3
.= (r * yy1) . i by PDIFF_1:def 1
.= r * y1i by RVSUM_1:44 ;
hence (proj (i,n)) . (r * y1) = r * ((proj (i,n)) . y1) by PDIFF_1:def 1; :: thesis: verum