let m be non empty Element of NAT ; :: thesis: for x, y being Point of (REAL-NS 1)
for i being Element of 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); :: thesis: for i being Element of 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 Element of NAT ; :: thesis: 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); :: thesis: ( 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 ) ; :: thesis: ( ((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:118;
reconsider qq2 = <*q2*> as Element of REAL 1 by FINSEQ_2:118;
( x - y = qq1 - qq2 & y - x = qq2 - qq1 ) by REAL_NS1:5, A2, A3;
then ( x - y = <*(q1 - q2)*> & y - x = <*(q2 - q1)*> ) by RVSUM_1:50;
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:97;
y = <*((proj i,m) . z)*> by A1, PDIFF_1:def 4;
then q2 = (proj i,m) . z1 by A2, A3, FINSEQ_1:97;
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, REAL_NS1:5, A2; :: thesis: verum