let p be FinSequence; :: thesis: for x being set st x in rng p holds
1 in dom p
let x be set ; :: thesis: ( x in rng p implies 1 in dom p )
assume x in rng p ; :: thesis: 1 in dom p
then p <> {} ;
then len p <> 0 ;
then ( 1 <= 1 & 1 <= len p & dom p = Seg (len p) ) by FINSEQ_1:def 3, NAT_1:14;
hence 1 in dom p by FINSEQ_1:3; :: thesis: verum