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
A4: len (p |-- x) = (len p) - (x .. p) by A1, Def7;
consider y being set such that
A5: y in dom (p |-- x) and
A6: (p |-- x) . y = x by A3, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A5;
A7: 1 <= y + (x .. p) by A1, Th31, NAT_1:12;
A8: y in Seg (len (p |-- x)) by A5, FINSEQ_1:def 3;
then y <= len (p |-- x) by FINSEQ_1:3;
then y + (x .. p) <= len p by A4, XREAL_1:21;
then y + (x .. p) in Seg (len p) by A7;
then A9: y + (x .. p) in dom p by FINSEQ_1:def 3;
A10: ( x .. p in dom p & p . (x .. p) = x ) by A1, Th29, Th30;
(p |-- x) . y = p . (y + (x .. p)) by A1, A5, Def7;
then 0 + (x .. p) = y + (x .. p) by A2, A6, A10, A9, FUNCT_1:def 8;
hence contradiction by A8, FINSEQ_1:3; :: thesis: verum