let m be non zero Nat; 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); 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; ( 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 )
; (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; verum