let p be FinSequence; :: thesis: for x being object st x in dom p holds
x <> 0
let x be object ; :: thesis: ( x in dom p implies x <> 0 )
assume x in dom p ; :: thesis: x <> 0
then x in Seg (len p) by FINSEQ_1:def 3;
hence x <> 0 by FINSEQ_1:1; :: thesis: verum