let p be FinSequence; 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 ; ( 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)
; 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; verum