let m be non zero Nat; :: thesis: for x being Element of REAL
for i being Nat st 1 <= i & i <= m & x <> 0 holds
Replace ((0* m),i,x) <> 0* m
let x be Element of REAL ; :: thesis: for i being Nat st 1 <= i & i <= m & x <> 0 holds
Replace ((0* m),i,x) <> 0* m
let i be Nat; :: thesis: ( 1 <= i & i <= m & x <> 0 implies Replace ((0* m),i,x) <> 0* m )
assume A1: ( 1 <= i & i <= m & x <> 0 ) ; :: thesis: Replace ((0* m),i,x) <> 0* m
then A2: i in Seg m ;
assume A3: Replace ((0* m),i,x) = 0* m ; :: thesis: contradiction
len (0* m) = m by CARD_1:def 7;
then Seg m = proj1 (0* m) by FINSEQ_1:def 3;
then x = (0* m) . i by A3, A2, FUNCT_7:31;
hence contradiction by A1; :: thesis: verum