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 CARD_1:def 7;
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:32;
hence (Replace ((0* m),i,x)) . j = 0 by A1, FINSEQ_2:57; :: 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:31; :: thesis: verum