let p be FinSequence; :: thesis: for x being set st p is one-to-one & x in rng p holds
{(x .. p)} = p " {x}
let x be set ; :: thesis: ( p is one-to-one & x in rng p implies {(x .. p)} = p " {x} )
assume that
A1: p is one-to-one and
A2: x in rng p ; :: thesis: {(x .. p)} = p " {x}
thus {(x .. p)} c= p " {x} :: according to XBOOLE_0:def 10 :: thesis: p " {x} c= {(x .. p)}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {(x .. p)} or y in p " {x} )
assume y in {(x .. p)} ; :: thesis: y in p " {x}
then y = x .. p by TARSKI:def 1;
hence y in p " {x} by A2, Th33; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in p " {x} or y in {(x .. p)} )
assume y in p " {x} ; :: thesis: y in {(x .. p)}
then ( y in dom p & p . y in {x} ) by FUNCT_1:def 13;
then ( y in dom p & p . y = x & p . (x .. p) = x & x .. p in dom p ) by A2, Th29, Th30, TARSKI:def 1;
then x .. p = y by A1, FUNCT_1:def 8;
hence y in {(x .. p)} by TARSKI:def 1; :: thesis: verum