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