let m, i be Element of 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 r be Real; :: thesis: ( ((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) )
reconsider p = ((reproj i,x) . r) - x as m -long FinSequence ;
reconsider q = (reproj i,(0* m)) . (r - ((proj i,m) . x)) as m -long FinSequence by FINSEQ_2:161;
reconsider s = x - ((reproj i,x) . r) as m -long FinSequence ;
reconsider t = (reproj i,(0* m)) . (((proj i,m) . x) - r) as m -long FinSequence by FINSEQ_2:161;
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:110;
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 ;
A3: ( len x = m & len (0* m) = m ) by A1, FINSEQ_1:def 3;
then A4: len (Replace x,i,r) = m by FINSEQ_7:7;
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:3;
then k in dom (Replace x,i,r) by A4, FINSEQ_3:27;
then A7: (Replace x,i,r) /. k = (Replace x,i,r) . k by PARTFUN1:def 8;
A8: p . k = (y1 . k) - (x1 . k) by RVSUM_1:48;
q = Replace (0* m),i,(r - ((proj i,m) . x)) by PDIFF_1:def 5;
then A9: q . k = (Replace (0* m),i,(r - ((proj i,m) . x))) /. k by A5, A1, PARTFUN1:def 8;

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:10;
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:12;
then ( (Replace x,i,r) . k = x1 . k & q . k = (m |-> 0 ) . k ) by A5, A1, PARTFUN1:def 8;
hence p . k = q . k by A2, A5, A1, A8, FINSEQ_2:71; :: thesis: verum

end;

end;

end;

hence ((reproj i,x) . r) - x = (reproj i,(0* m)) . (r - ((proj i,m) . x)) by A1, FINSEQ_1:17; :: thesis: x - ((reproj i,x) . r) = (reproj i,(0* m)) . (((proj i,m) . x) - r)
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:3;
then k in dom (Replace x,i,r) by A4, FINSEQ_3:27;
then A13: (Replace x,i,r) /. k = (Replace x,i,r) . k by PARTFUN1:def 8;
A14: s . k = (x1 . k) - (y1 . k) by RVSUM_1:48;
t = Replace (0* m),i,(((proj i,m) . x) - r) by PDIFF_1:def 5;
then A15: t . k = (Replace (0* m),i,(((proj i,m) . x) - r)) /. k by A1, A11, PARTFUN1:def 8;

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:10;
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:12;
then ( (Replace x,i,r) . k = x1 . k & t . k = (m |-> 0 ) . k ) by A1, A11, PARTFUN1:def 8;
hence s . k = t . k by A2, A1, A11, A14, FINSEQ_2:71; :: thesis: verum

end;

end;

end;

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