let i, n 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)) . y1 = <*((proj (i,n)) . y1)*> by PDIFF_1:def 4;
then A1: (Proj (i,n)) . y1 = <*y1i*> by PDIFF_1:def 1;
A2: <*y1i*> is Element of REAL 1 by FINSEQ_2:98;
(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:44
.= r * <*y1i*> by RVSUM_1:47 ;
hence (Proj (i,n)) . (r * y1) = r * ((Proj (i,n)) . y1) by A1, A2, REAL_NS1:3; :: thesis: verum