let m be non empty Element of NAT ; :: thesis: for x, y being Point of (REAL-NS 1)
for i being Element of NAT st 1 <= i & i <= m holds
(reproj i,(0. (REAL-NS m))) . (x + y) = ((reproj i,(0. (REAL-NS m))) . x) + ((reproj i,(0. (REAL-NS m))) . y)
let x, y be Point of (REAL-NS 1); :: thesis: for i being Element of NAT st 1 <= i & i <= m holds
(reproj i,(0. (REAL-NS m))) . (x + y) = ((reproj i,(0. (REAL-NS m))) . x) + ((reproj i,(0. (REAL-NS m))) . y)
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= m implies (reproj i,(0. (REAL-NS m))) . (x + y) = ((reproj i,(0. (REAL-NS m))) . x) + ((reproj i,(0. (REAL-NS m))) . y) )
assume A1: ( 1 <= i & i <= m ) ; :: thesis: (reproj i,(0. (REAL-NS m))) . (x + y) = ((reproj i,(0. (REAL-NS m))) . x) + ((reproj i,(0. (REAL-NS m))) . y)
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 q2 being Element of REAL , z2 being Element of REAL m such that
A3: ( y = <*q2*> & z2 = 0. (REAL-NS m) & (reproj i,(0. (REAL-NS m))) . y = (reproj i,z2) . q2 ) by PDIFF_1:def 6;
consider q12 being Element of REAL , z12 being Element of REAL m such that
A4: ( x + y = <*q12*> & z12 = 0. (REAL-NS m) & (reproj i,(0. (REAL-NS m))) . (x + y) = (reproj i,z12) . q12 ) by PDIFF_1:def 6;
A5: 0. (REAL-NS m) = 0* m by REAL_NS1:def 4;
reconsider qq1 = <*q1*> as Element of REAL 1 by FINSEQ_2:118;
reconsider qq2 = <*q2*> as Element of REAL 1 by FINSEQ_2:118;
x + y = qq1 + qq2 by REAL_NS1:2, A2, A3;
then A6: x + y = <*(q1 + q2)*> by RVSUM_1:29;
((reproj i,(0. (REAL-NS m))) . x) + ((reproj i,(0. (REAL-NS m))) . y) = ((reproj i,(0* m)) . q1) + ((reproj i,(0* m)) . q2) by A2, A3, A5, REAL_NS1:2
.= (reproj i,(0* m)) . (q1 + q2) by A1, Th13 ;
hence (reproj i,(0. (REAL-NS m))) . (x + y) = ((reproj i,(0. (REAL-NS m))) . x) + ((reproj i,(0. (REAL-NS m))) . y) by A6, A4, A5, FINSEQ_1:97; :: thesis: verum