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