let m be non zero Nat; :: thesis: for x being Point of (REAL-NS 1)
for a being Real
for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x)
let x be Point of (REAL-NS 1); :: thesis: for a being Real
for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x)
let a be Real; :: thesis: for i being Nat st 1 <= i & i <= m holds
(reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x)
let i be Nat; :: thesis: ( 1 <= i & i <= m implies (reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x) )
assume A1: ( 1 <= i & i <= m ) ; :: thesis: (reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x)
consider q1 being Element of REAL , z1 being Element of REAL m such that
A2: ( x = <*q1*> & z1 = 0. (REAL-NS m) & (reproj (i,(0. (REAL-NS m)))) . x = (reproj (i,z1)) . q1 ) by PDIFF_1:def 6;
consider q12 being Element of REAL , z12 being Element of REAL m such that
A3: ( a * x = <*q12*> & z12 = 0. (REAL-NS m) & (reproj (i,(0. (REAL-NS m)))) . (a * x) = (reproj (i,z12)) . q12 ) by PDIFF_1:def 6;
A4: 0. (REAL-NS m) = 0* m by REAL_NS1:def 4;
reconsider qq1 = <*q1*> as Element of REAL 1 by FINSEQ_2:98;
a * x = a * qq1 by A2, REAL_NS1:3;
then A5: a * x = <*(a * q1)*> by RVSUM_1:47;
a * ((reproj (i,(0. (REAL-NS m)))) . x) = a * ((reproj (i,(0* m))) . q1) by A2, A4, REAL_NS1:3
.= (reproj (i,(0* m))) . (a * q1) by A1, Th15 ;
hence (reproj (i,(0. (REAL-NS m)))) . (a * x) = a * ((reproj (i,(0. (REAL-NS m)))) . x) by A5, A3, A4, FINSEQ_1:76; :: thesis: verum