let m be non zero Nat; :: thesis: for x, y being Element of REAL
for z being Element of REAL m
for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
let x, y be Element of REAL ; :: thesis: for z being Element of REAL m
for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
let z be Element of REAL m; :: thesis: for i being Nat st 1 <= i & i <= m & y = (proj (i,m)) . z holds
( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
let i be Nat; :: thesis: ( 1 <= i & i <= m & y = (proj (i,m)) . z implies ( (Replace (z,i,x)) - z = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (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 = (0* m) +* (i,(x - y)) & z - (Replace (z,i,x)) = (0* m) +* (i,(y - x)) )
reconsider xy = x - y, my = - y as Element of REAL ;
A3: ( len (Replace ((0* m),i,xy)) = m & len (Replace ((0* m),i,x)) = m & len (Replace ((0* m),i,my)) = m ) by Lm6;
A4: dom (Replace (z,i,x)) = dom z by FUNCT_7:30;
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 CARD_1:def 7;
dom ((Replace (z,i,x)) - z) = Seg m by A4, A5, A6, FINSEQ_1:89;
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,xy)) by FINSEQ_7:5;
for j being Nat st 1 <= j & j <= len ((Replace (z,i,x)) - z) holds
(Replace ((0* m),i,xy)) . 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,xy)) . j = ((Replace (z,i,x)) - z) . j )
assume A9: ( 1 <= j & j <= len ((Replace (z,i,x)) - z) ) ; :: thesis: (Replace ((0* m),i,xy)) . j = ((Replace (z,i,x)) - z) . j
reconsider j = j as Nat ;
A10: j in dom ((Replace (z,i,x)) - z) by A9, FINSEQ_3:25;
(- z) . j = (- 1) * (z . j) by RVSUM_1:44;
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:25;
hence (Replace (z,i,x)) . i = x by FUNCT_7:31; :: thesis: verum

end;

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

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

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

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

end;

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

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

end;

end;

end;

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