let m, i be Nat; :: thesis: for x being Element of REAL m
for r being Real holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0* m))) . (r - ((proj (i,m)) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r) )
let x be Element of REAL m; :: thesis: for r being Real holds
( ((reproj (i,x)) . r) - x = (reproj (i,(0* m))) . (r - ((proj (i,m)) . x)) & x - ((reproj (i,x)) . r) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r) )
let r1 be Real; :: thesis: ( ((reproj (i,x)) . r1) - x = (reproj (i,(0* m))) . (r1 - ((proj (i,m)) . x)) & x - ((reproj (i,x)) . r1) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r1) )
reconsider r = r1 as Element of REAL by XREAL_0:def 1;
reconsider rr = r - ((proj (i,m)) . x) as Element of REAL ;
reconsider rs = ((proj (i,m)) . x) - r as Element of REAL ;
reconsider p = ((reproj (i,x)) . r) - x as m -element FinSequence ;
reconsider q = (reproj (i,(0* m))) . rr as m -element FinSequence ;
reconsider s = x - ((reproj (i,x)) . r) as m -element FinSequence ;
reconsider t = (reproj (i,(0* m))) . rs as m -element FinSequence ;
A1: ( dom p = Seg m & dom q = Seg m & dom s = Seg m & dom t = Seg m & dom x = Seg m & dom (0* m) = Seg m ) by FINSEQ_1:89;
reconsider x1 = x as Element of m -tuples_on REAL ;
A2: (reproj (i,x)) . r = Replace (x,i,r) by PDIFF_1:def 5;
reconsider y1 = (reproj (i,x)) . r as Element of m -tuples_on REAL ;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A3: ( len x = mm & len (0* m) = mm ) by A1, FINSEQ_1:def 3;
then A4: len (Replace (x,i,r)) = m by FINSEQ_7:5;
for k being Nat st k in dom p holds
p . k = q . k

proof

let k be Nat; :: thesis: ( k in dom p implies p . k = q . k )
assume A5: k in dom p ; :: thesis: p . k = q . k
then A6: ( 1 <= k & k <= m ) by A1, FINSEQ_1:1;
then k in dom (Replace (x,i,r)) by A4, FINSEQ_3:25;
then A7: (Replace (x,i,r)) /. k = (Replace (x,i,r)) . k by PARTFUN1:def 6;
A8: p . k = (y1 . k) - (x1 . k) by RVSUM_1:27;
q = Replace ((0* m),i,rr) by PDIFF_1:def 5;
then A9: q . k = (Replace ((0* m),i,rr)) /. k by A5, A1, PARTFUN1:def 6;

per cases ( k = i or k <> i ) ;

suppose A10: k = i ; :: thesis: p . k = q . k

then ( p . k = r - (x1 . k) & q . k = r - ((proj (i,m)) . x) ) by A2, A3, A6, A7, A8, A9, FINSEQ_7:8;
hence p . k = q . k by A10, PDIFF_1:def 1; :: thesis: verum

end;

suppose k <> i ; :: thesis: p . k = q . k

then ( (Replace (x,i,r)) . k = x1 /. k & q . k = (0* m) /. k ) by A3, A6, A7, A9, FINSEQ_7:10;
then ( (Replace (x,i,r)) . k = x1 . k & q . k = (m |-> 0) . k ) by A5, A1, PARTFUN1:def 6;
hence p . k = q . k by A2, A8; :: thesis: verum

end;

end;

end;

then ((reproj (i,x)) . r) - x = (reproj (i,(0* m))) . (r - ((proj (i,m)) . x)) by A1, FINSEQ_1:13;
hence ((reproj (i,x)) . r1) - x = (reproj (i,(0* m))) . (r1 - ((proj (i,m)) . x)) ; :: thesis: x - ((reproj (i,x)) . r1) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r1)
for k being Nat st k in dom s holds
s . k = t . k

proof

let k be Nat; :: thesis: ( k in dom s implies s . k = t . k )
assume A11: k in dom s ; :: thesis: s . k = t . k
then A12: ( 1 <= k & k <= m ) by A1, FINSEQ_1:1;
then k in dom (Replace (x,i,r)) by A4, FINSEQ_3:25;
then A13: (Replace (x,i,r)) /. k = (Replace (x,i,r)) . k by PARTFUN1:def 6;
A14: s . k = (x1 . k) - (y1 . k) by RVSUM_1:27;
t = Replace ((0* m),i,rs) by PDIFF_1:def 5;
then A15: t . k = (Replace ((0* m),i,rs)) /. k by A1, A11, PARTFUN1:def 6;

per cases ( k = i or k <> i ) ;

suppose A16: k = i ; :: thesis: s . k = t . k

then ( s . k = (x1 . k) - r & t . k = ((proj (i,m)) . x) - r ) by A2, A3, A12, A13, A14, A15, FINSEQ_7:8;
hence s . k = t . k by A16, PDIFF_1:def 1; :: thesis: verum

end;

suppose k <> i ; :: thesis: s . k = t . k

then ( (Replace (x,i,r)) . k = x1 /. k & t . k = (0* m) /. k ) by A3, A12, A13, A15, FINSEQ_7:10;
then ( (Replace (x,i,r)) . k = x1 . k & t . k = (m |-> 0) . k ) by A1, A11, PARTFUN1:def 6;
hence s . k = t . k by A2, A14; :: thesis: verum

end;

end;

end;

hence x - ((reproj (i,x)) . r1) = (reproj (i,(0* m))) . (((proj (i,m)) . x) - r1) by A1, FINSEQ_1:13; :: thesis: verum