let m be non zero Nat; for x, y being Element of REAL
for i being Nat st 1 <= i & i <= m holds
Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y))
let x, y be Element of REAL ; for i being Nat st 1 <= i & i <= m holds
Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y))
let i be Nat; ( 1 <= i & i <= m implies Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y)) )
assume A1:
( 1 <= i & i <= m )
; Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y))
reconsider xy = x + y as Element of REAL ;
A2:
( len (Replace ((0* m),i,xy)) = m & len (Replace ((0* m),i,x)) = m & len (Replace ((0* m),i,y)) = m )
by Lm6;
then A3:
len ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) = len (Replace ((0* m),i,xy))
by RVSUM_1:115;
for j being Nat st 1 <= j & j <= len (Replace ((0* m),i,xy)) holds
(Replace ((0* m),i,xy)) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j
proof
let j be
Nat;
( 1 <= j & j <= len (Replace ((0* m),i,xy)) implies (Replace ((0* m),i,xy)) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j )
assume A4:
( 1
<= j &
j <= len (Replace ((0* m),i,xy)) )
;
(Replace ((0* m),i,xy)) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j
reconsider j =
j as
Nat ;
A5:
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 A4, A2, FINSEQ_3:25;
then
j in dom ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y)))
by A5, XBOOLE_0:def 4;
then A6:
((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 i <> j )
;
suppose A7:
i = j
;
(Replace ((0* m),i,xy)) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . jthen ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j =
x + ((Replace ((0* m),i,y)) . j)
by A1, A6, Lm7
.=
x + y
by A1, A7, Lm7
;
hence
(Replace ((0* m),i,xy)) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j
by A1, A7, Lm7;
verum end; suppose A8:
i <> j
;
(Replace ((0* m),i,xy)) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . jthen ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j =
0 + ((Replace ((0* m),i,y)) . j)
by A4, A6, A2, Lm7
.=
0
by A4, A2, A8, Lm7
;
hence
(Replace ((0* m),i,xy)) . j = ((Replace ((0* m),i,x)) + (Replace ((0* m),i,y))) . j
by A4, A2, A8, Lm7;
verum end;
end;
hence
Replace ((0* m),i,(x + y)) = (Replace ((0* m),i,x)) + (Replace ((0* m),i,y))
by A3; verum