let p be FinSequence; :: thesis: for x being object st x in rng p & p is one-to-one holds
not x in rng (p |-- x)
let x be object ; :: 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, Def6;
consider y being object such that
A5: y in dom (p |-- x) and
A6: (p |-- x) . y = x by A3, FUNCT_1:def 3;
reconsider y = y as Element of NAT by A5;
A7: 1 <= y + (x .. p) by A1, Th21, NAT_1:12;
A8: y in Seg (len (p |-- x)) by A5, FINSEQ_1:def 3;
then y <= len (p |-- x) by FINSEQ_1:1;
then y + (x .. p) <= len p by A4, XREAL_1:19;
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, Th19, Th20;
(p |-- x) . y = p . (y + (x .. p)) by A1, A5, Def6;
then 0 + (x .. p) = y + (x .. p) by A2, A6, A10, A9;
hence contradiction by A8, FINSEQ_1:1; :: thesis: verum