let f be FinSequence; :: thesis: for x being set holds
( x in rng f or x .. f = 0 )
let x be set ; :: thesis: ( x in rng f or x .. f = 0 )
assume A1: not x in rng f ; :: thesis: x .. f = 0

A2: now :: thesis: not f " {x} <> {}

assume f " {x} <> {} ; :: thesis: contradiction
then consider y being object such that
A3: y in f " {x} by XBOOLE_0:def 1;
f . y in {x} by A3, FUNCT_1:def 7;
then A4: f . y = x by TARSKI:def 1;
y in dom f by A3, FUNCT_1:def 7;
hence contradiction by A1, A4, FUNCT_1:3; :: thesis: verum

end;

thus x .. f = (Sgm (f " {x})) . 1 by FINSEQ_4:def 4
.= 0 by A2, FINSEQ_3:43 ; :: thesis: verum