let m be non zero Nat; for x, y being Point of (REAL-NS 1)
for i being Nat
for z being Point of (REAL-NS m) st 1 <= i & i <= m & y = (Proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0. (REAL-NS m)))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0. (REAL-NS m)))) . (y - x) )
let x, y be Point of (REAL-NS 1); for i being Nat
for z being Point of (REAL-NS m) st 1 <= i & i <= m & y = (Proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0. (REAL-NS m)))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0. (REAL-NS m)))) . (y - x) )
let i be Nat; for z being Point of (REAL-NS m) st 1 <= i & i <= m & y = (Proj (i,m)) . z holds
( ((reproj (i,z)) . x) - z = (reproj (i,(0. (REAL-NS m)))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0. (REAL-NS m)))) . (y - x) )
let z be Point of (REAL-NS m); ( 1 <= i & i <= m & y = (Proj (i,m)) . z implies ( ((reproj (i,z)) . x) - z = (reproj (i,(0. (REAL-NS m)))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0. (REAL-NS m)))) . (y - x) ) )
assume A1:
( 1 <= i & i <= m & y = (Proj (i,m)) . z )
; ( ((reproj (i,z)) . x) - z = (reproj (i,(0. (REAL-NS m)))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0. (REAL-NS m)))) . (y - x) )
consider q1 being Element of REAL , z1 being Element of REAL m such that
A2:
( x = <*q1*> & z1 = z & (reproj (i,z)) . 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 = z & (reproj (i,z)) . 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;
consider q21 being Element of REAL , z21 being Element of REAL m such that
A5:
( y - x = <*q21*> & z21 = 0. (REAL-NS m) & (reproj (i,(0. (REAL-NS m)))) . (y - x) = (reproj (i,z21)) . q21 )
by PDIFF_1:def 6;
A6:
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 & y - x = qq2 - qq1 )
by A2, A3, REAL_NS1:5;
then
( x - y = <*(q1 - q2)*> & y - x = <*(q2 - q1)*> )
by RVSUM_1:29;
then A7:
( (reproj (i,(0. (REAL-NS m)))) . (x - y) = (reproj (i,(0* m))) . (q1 - q2) & (reproj (i,(0. (REAL-NS m)))) . (y - x) = (reproj (i,(0* m))) . (q2 - q1) )
by A4, A5, A6, FINSEQ_1:76;
y = <*((proj (i,m)) . z)*>
by A1, PDIFF_1:def 4;
then
q2 = (proj (i,m)) . z1
by A2, A3, FINSEQ_1:76;
then
( ((reproj (i,z1)) . q1) - z1 = (reproj (i,(0* m))) . (q1 - q2) & z1 - ((reproj (i,z1)) . q1) = (reproj (i,(0* m))) . (q2 - q1) )
by Th19, A1;
hence
( ((reproj (i,z)) . x) - z = (reproj (i,(0. (REAL-NS m)))) . (x - y) & z - ((reproj (i,z)) . x) = (reproj (i,(0. (REAL-NS m)))) . (y - x) )
by A7, A2, REAL_NS1:5; verum