let x be set ; :: thesis: for A being FinSequence st A <- x = 0 holds
x nin rng A
let A be FinSequence; :: thesis: ( A <- x = 0 implies x nin rng A )
assume ( A <- x = 0 & x in rng A ) ; :: thesis: contradiction
then 0 in dom A by Th16;
hence contradiction by FINSEQ_3:24; :: thesis: verum