let x be set ; :: thesis: for A being FinSequence st x nin rng A holds
A <- x = 0
let A be FinSequence; :: thesis: ( x nin rng A implies A <- x = 0 )
assume x nin rng A ; :: thesis: A <- x = 0
then A " {x} = {} by FUNCT_1:72;
hence A <- x = 0 by SETFAM_1:def 1; :: thesis: verum