let m be non empty Element of NAT ; :: thesis: for x, y being Element of REAL
for z being Element of REAL m
for i being Element of NAT st 1 <= i & i <= m & y = (proj i,m) . z holds
( (Replace z,i,x) - z = Replace (0* m),i,(x - y) & z - (Replace z,i,x) = Replace (0* m),i,(y - x) )
let x, y be Element of REAL ; :: thesis: for z being Element of REAL m
for i being Element of NAT st 1 <= i & i <= m & y = (proj i,m) . z holds
( (Replace z,i,x) - z = Replace (0* m),i,(x - y) & z - (Replace z,i,x) = Replace (0* m),i,(y - x) )
let z be Element of REAL m; :: thesis: for i being Element of NAT st 1 <= i & i <= m & y = (proj i,m) . z holds
( (Replace z,i,x) - z = Replace (0* m),i,(x - y) & z - (Replace z,i,x) = Replace (0* m),i,(y - x) )
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= m & y = (proj i,m) . z implies ( (Replace z,i,x) - z = Replace (0* m),i,(x - y) & z - (Replace z,i,x) = Replace (0* m),i,(y - x) ) )
assume that
A1: ( 1 <= i & i <= m ) and
A2: y = (proj i,m) . z ; :: thesis: ( (Replace z,i,x) - z = Replace (0* m),i,(x - y) & z - (Replace z,i,x) = Replace (0* m),i,(y - x) )
A3: ( len (Replace (0* m),i,(x - y)) = m & len (Replace (0* m),i,x) = m & len (Replace (0* m),i,(- y)) = m ) by Lm6;
A4: dom (Replace z,i,x) = dom z by FUNCT_7:32;
A5: ( dom (- z) = dom z & dom (- (Replace z,i,x)) = dom (Replace z,i,x) ) by VALUED_1:def 5;
A6: dom ((Replace z,i,x) - z) = (dom (Replace z,i,x)) /\ (dom (- z)) by VALUED_1:def 1;
A7: len (0* m) = m by FINSEQ_1:def 18;
dom ((Replace z,i,x) - z) = Seg m by A4, A5, A6, EUCLID:3;
then len ((Replace z,i,x) - z) = len (0* m) by A7, FINSEQ_1:def 3;
then A8: len ((Replace z,i,x) - z) = len (Replace (0* m),i,(x - y)) by FINSEQ_7:7;
for j being Nat st 1 <= j & j <= len ((Replace z,i,x) - z) holds
(Replace (0* m),i,(x - y)) . j = ((Replace z,i,x) - z) . j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len ((Replace z,i,x) - z) implies (Replace (0* m),i,(x - y)) . j = ((Replace z,i,x) - z) . j )
assume A9: ( 1 <= j & j <= len ((Replace z,i,x) - z) ) ; :: thesis: (Replace (0* m),i,(x - y)) . j = ((Replace z,i,x) - z) . j
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A10: j in dom ((Replace z,i,x) - z) by A9, FINSEQ_3:27;
(- z) . j = (- 1) * (z . j) by RVSUM_1:66;
then ((Replace z,i,x) - z) . j = ((Replace z,i,x) . j) + (- (z . j)) by A10, VALUED_1:def 1;
then A11: ((Replace z,i,x) - z) . j = ((Replace z,i,x) . j) - (z . j) ;
A12: ( 1 <= i & i <= len z implies (Replace z,i,x) . i = x )

proof

assume ( 1 <= i & i <= len z ) ; :: thesis: (Replace z,i,x) . i = x
then i in dom z by FINSEQ_3:27;
hence (Replace z,i,x) . i = x by FUNCT_7:33; :: thesis: verum

end;

A13: dom ((Replace (0* m),i,x) + (Replace (0* m),i,(- y))) = (dom (Replace (0* m),i,x)) /\ (dom (Replace (0* m),i,(- y))) by VALUED_1:def 1;
( j in dom (Replace (0* m),i,x) & j in dom (Replace (0* m),i,(- y)) ) by A3, A9, A8, FINSEQ_3:27;
then j in dom ((Replace (0* m),i,x) + (Replace (0* m),i,(- y))) by A13, XBOOLE_0:def 4;
then A14: ((Replace (0* m),i,x) + (Replace (0* m),i,(- y))) . j = ((Replace (0* m),i,x) . j) + ((Replace (0* m),i,(- y)) . j) by VALUED_1:def 1;

per cases ( i = j or not i = j ) ;

suppose A15: i = j ; :: thesis: (Replace (0* m),i,(x - y)) . j = ((Replace z,i,x) - z) . j

(Replace (0* m),i,(x - y)) . j = (Replace (0* m),i,(x + (- y))) . j
.= ((Replace (0* m),i,x) + (Replace (0* m),i,(- y))) . j by A1, Th9
.= x + ((Replace (0* m),i,(- y)) . j) by A1, A14, A15, Lm7
.= x + (- y) by A1, A15, Lm7
.= x - ((proj i,m) . z) by A2 ;
hence (Replace (0* m),i,(x - y)) . j = ((Replace z,i,x) - z) . j by A11, A9, A4, A5, A6, FINSEQ_3:31, A12, A15, PDIFF_1:def 1; :: thesis: verum

end;

suppose A16: not i = j ; :: thesis: (Replace (0* m),i,(x - y)) . j = ((Replace z,i,x) - z) . j

then (Replace (0* m),i,(x - y)) . j = (z . j) - (z . j) by A3, A9, A8, Lm7;
hence (Replace (0* m),i,(x - y)) . j = ((Replace z,i,x) - z) . j by A11, A16, FUNCT_7:34; :: thesis: verum

end;

end;

end;

hence A17: (Replace z,i,x) - z = Replace (0* m),i,(x - y) by A8, FINSEQ_1:18; :: thesis: z - (Replace z,i,x) = Replace (0* m),i,(y - x)
reconsider a = - 1 as Element of REAL by XREAL_0:def 1;
z - (Replace z,i,x) = - (Replace (0* m),i,(x - y)) by A17, RVSUM_1:56;
then z - (Replace z,i,x) = Replace (0* m),i,(a * (x - y)) by A1, Th10;
hence z - (Replace z,i,x) = Replace (0* m),i,(y - x) ; :: thesis: verum