let m be non zero Nat; :: thesis: for x, y being Point of (REAL-NS 1)
for i being 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 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 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:98;
reconsider qq2 = <*q2*> as Element of REAL 1 by FINSEQ_2:98;
x + y = qq1 + qq2 by A2, A3, REAL_NS1:2;
then A6: x + y = <*(q1 + q2)*> by RVSUM_1:13;
((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:76; :: thesis: verum