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