let m be non zero Nat; 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 ; for i being Nat st 1 <= i & i <= m & x <> 0 holds
Replace ((0* m),i,x) <> 0* m
let i be Nat; ( 1 <= i & i <= m & x <> 0 implies Replace ((0* m),i,x) <> 0* m )
assume A1:
( 1 <= i & i <= m & x <> 0 )
; Replace ((0* m),i,x) <> 0* m
then A2:
i in Seg m
;
assume A3:
Replace ((0* m),i,x) = 0* m
; 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; verum