let m, i be Element of NAT ; :: thesis: for x being Point of (REAL-NS m)
for p being Point of (REAL-NS 1) holds
( ((reproj i,x) . p) - x = (reproj i,(0. (REAL-NS m))) . (p - ((Proj i,m) . x)) & x - ((reproj i,x) . p) = (reproj i,(0. (REAL-NS m))) . (((Proj i,m) . x) - p) )
let x be Point of (REAL-NS m); :: thesis: for p being Point of (REAL-NS 1) holds
( ((reproj i,x) . p) - x = (reproj i,(0. (REAL-NS m))) . (p - ((Proj i,m) . x)) & x - ((reproj i,x) . p) = (reproj i,(0. (REAL-NS m))) . (((Proj i,m) . x) - p) )
let p be Point of (REAL-NS 1); :: thesis: ( ((reproj i,x) . p) - x = (reproj i,(0. (REAL-NS m))) . (p - ((Proj i,m) . x)) & x - ((reproj i,x) . p) = (reproj i,(0. (REAL-NS m))) . (((Proj i,m) . x) - p) )
consider p1 being Element of REAL , y being Element of REAL m such that
A1: ( p = <*p1*> & y = x & (reproj i,x) . p = (reproj i,y) . p1 ) by PDIFF_1:def 6;
reconsider pm = p as Element of REAL 1 by REAL_NS1:def 4;
reconsider rm = (reproj i,y) . p1 as Element of REAL m ;
((reproj i,x) . p) - x = rm - y by A1, REAL_NS1:5;
then A2: ((reproj i,x) . p) - x = (reproj i,(0* m)) . (p1 - ((proj i,m) . y)) by Th6;
A3: 0* m = 0. (REAL-NS m) by REAL_NS1:def 4;
A4: <*((proj i,m) . y)*> = (Proj i,m) . x by A1, PDIFF_1:def 4;
reconsider Pr = (Proj i,m) . x as Element of REAL 1 by REAL_NS1:def 4;
consider r1 being Element of REAL , z being Element of REAL m such that
A5: ( p - ((Proj i,m) . x) = <*r1*> & z = 0. (REAL-NS m) & (reproj i,(0. (REAL-NS m))) . (p - ((Proj i,m) . x)) = (reproj i,z) . r1 ) by PDIFF_1:def 6;
p - ((Proj i,m) . x) = pm - Pr by REAL_NS1:5;
then p - ((Proj i,m) . x) = <*(p1 - ((proj i,m) . y))*> by A1, A4, RVSUM_1:50;
hence ((reproj i,x) . p) - x = (reproj i,(0. (REAL-NS m))) . (p - ((Proj i,m) . x)) by A2, A3, A5, FINSEQ_1:97; :: thesis: x - ((reproj i,x) . p) = (reproj i,(0. (REAL-NS m))) . (((Proj i,m) . x) - p)
x - ((reproj i,x) . p) = y - rm by A1, REAL_NS1:5;
then A6: x - ((reproj i,x) . p) = (reproj i,(0* m)) . (((proj i,m) . y) - p1) by Th6;
consider r2 being Element of REAL , z being Element of REAL m such that
A7: ( ((Proj i,m) . x) - p = <*r2*> & z = 0. (REAL-NS m) & (reproj i,(0. (REAL-NS m))) . (((Proj i,m) . x) - p) = (reproj i,z) . r2 ) by PDIFF_1:def 6;
((Proj i,m) . x) - p = Pr - pm by REAL_NS1:5;
then ((Proj i,m) . x) - p = <*(((proj i,m) . y) - p1)*> by A1, A4, RVSUM_1:50;
hence x - ((reproj i,x) . p) = (reproj i,(0. (REAL-NS m))) . (((Proj i,m) . x) - p) by A3, A7, A6, FINSEQ_1:97; :: thesis: verum