let m, i be 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:29;
hence ((reproj (i,x)) . p) - x = (reproj (i,(0. (REAL-NS m)))) . (p - ((Proj (i,m)) . x)) by A2, A3, A5, FINSEQ_1:76; :: 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:29;
hence x - ((reproj (i,x)) . p) = (reproj (i,(0. (REAL-NS m)))) . (((Proj (i,m)) . x) - p) by A3, A7, A6, FINSEQ_1:76; :: thesis: verum