let p be FinSequence; :: thesis: for x being set st x in rng p holds
x .. p in dom p
let x be set ; :: thesis: ( x in rng p implies x .. p in dom p )
A1: ( p " {x} c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def 3, RELAT_1:167;
assume x in rng p ; :: thesis: x .. p in dom p
then p " {x} <> {} by FUNCT_1:142;
then rng (Sgm (p " {x})) <> {} by A1, FINSEQ_1:def 13;
then 1 in dom (Sgm (p " {x})) by FINSEQ_3:34;
then x .. p in rng (Sgm (p " {x})) by FUNCT_1:def 5;
then x .. p in p " {x} by A1, FINSEQ_1:def 13;
hence x .. p in dom p by FUNCT_1:def 13; :: thesis: verum