let m be non empty Element of NAT ; :: thesis: for x being Element of REAL
for i, j being Element of NAT st 1 <= j & j <= m holds
( ( i = j implies (Replace (0* m),i,x) . j = x ) & ( i <> j implies (Replace (0* m),i,x) . j = 0 ) )
let x be Element of REAL ; :: thesis: for i, j being Element of NAT st 1 <= j & j <= m holds
( ( i = j implies (Replace (0* m),i,x) . j = x ) & ( i <> j implies (Replace (0* m),i,x) . j = 0 ) )
let i, j be Element of NAT ; :: thesis: ( 1 <= j & j <= m implies ( ( i = j implies (Replace (0* m),i,x) . j = x ) & ( i <> j implies (Replace (0* m),i,x) . j = 0 ) ) )
assume ( 1 <= j & j <= m ) ; :: thesis: ( ( i = j implies (Replace (0* m),i,x) . j = x ) & ( i <> j implies (Replace (0* m),i,x) . j = 0 ) )
then A1: j in Seg m ;
len (0* m) = m by FINSEQ_1:def 18;
then A2: j in dom (0* m) by A1, FINSEQ_1:def 3;

now

assume i <> j ; :: thesis: (Replace (0* m),i,x) . j = 0
then ((0* m) +* i,x) . j = (0* m) . j by FUNCT_7:34;
hence (Replace (0* m),i,x) . j = 0 by A1, FINSEQ_2:71; :: thesis: verum

end;

hence ( ( i = j implies (Replace (0* m),i,x) . j = x ) & ( i <> j implies (Replace (0* m),i,x) . j = 0 ) ) by A2, FUNCT_7:33; :: thesis: verum