let p be FinSequence; :: thesis: for x being set st x in rng p & p is one-to-one holds
not x in rng (p |-- x)
let x be set ; :: thesis: ( x in rng p & p is one-to-one implies not x in rng (p |-- x) )
assume that
A1: x in rng p and
A2: p is one-to-one and
A3: x in rng (p |-- x) ; :: thesis: contradiction
consider y being set such that
A4: y in dom (p |-- x) and
A5: (p |-- x) . y = x by A3, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A4;
A6: (p |-- x) . y = p . (y + (x .. p)) by A1, A4, Def7;
A7: ( x .. p in dom p & p . (x .. p) = x ) by A1, Th29, Th30;
( 1 <= x .. p & x .. p <= y + (x .. p) ) by A1, Th31, NAT_1:12;
then A8: 1 <= y + (x .. p) by XXREAL_0:2;
A9: y in Seg (len (p |-- x)) by A4, FINSEQ_1:def 3;
then ( y <= len (p |-- x) & len (p |-- x) = (len p) - (x .. p) ) by A1, Def7, FINSEQ_1:3;
then y + (x .. p) <= len p by XREAL_1:21;
then y + (x .. p) in Seg (len p) by A8;
then y + (x .. p) in dom p by FINSEQ_1:def 3;
then 0 + (x .. p) = y + (x .. p) by A2, A5, A6, A7, FUNCT_1:def 8;
hence contradiction by A9, FINSEQ_1:3; :: thesis: verum