let m be non zero Nat; :: thesis: for x being Real
for i, j being 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 Real; :: thesis: for i, j being 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 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 :: thesis: ( i <> j implies (Replace ((0* m),i,x)) . j = 0 )

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 ; :: 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