let p be FinSequence; :: thesis: for x being object st x in rng p holds
p . (x .. p) = x
let x be object ; :: thesis: ( x in rng p implies p . (x .. p) = x )
set q = Sgm (p " {x});
( p " {x} c= dom p & dom p = Seg (len p) ) by FINSEQ_1:def 3, RELAT_1:132;
then a1: p " {x} is included_in_Seg ;
assume x in rng p ; :: thesis: p . (x .. p) = x
then p " {x} <> {} by FUNCT_1:72;
then rng (Sgm (p " {x})) <> {} by a1, FINSEQ_1:def 14;
then 1 in dom (Sgm (p " {x})) by FINSEQ_3:32;
then A2: (Sgm (p " {x})) . 1 in rng (Sgm (p " {x})) by FUNCT_1:def 3;
rng (Sgm (p " {x})) = p " {x} by a1, FINSEQ_1:def 14;
then p . (x .. p) in {x} by A2, FUNCT_1:def 7;
hence p . (x .. p) = x by TARSKI:def 1; :: thesis: verum