let p be FinSequence; :: thesis: for x being object st p is one-to-one & x in rng p holds
{(x .. p)} = p " {x}
let x be object ; :: 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 object ; :: 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, Th23; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in p " {x} or y in {(x .. p)} )
assume A3: y in p " {x} ; :: thesis: y in {(x .. p)}
then A4: y in dom p by FUNCT_1:def 7;
p . y in {x} by A3, FUNCT_1:def 7;
then A5: p . y = x by TARSKI:def 1;
( p . (x .. p) = x & x .. p in dom p ) by A2, Th19, Th20;
then x .. p = y by A1, A4, A5;
hence y in {(x .. p)} by TARSKI:def 1; :: thesis: verum