let p be FinSequence; for x being object st x in rng p holds
not x in rng (p -| x)
let x be object ; ( x in rng p implies not x in rng (p -| x) )
assume that
A1:
x in rng p
and
A2:
x in rng (p -| x)
; contradiction
reconsider n = (x .. p) - 1 as Element of NAT by A1, Th22;
set r = p | (Seg n);
A3:
p | (Seg n) = p -| x
by A1, Th33;
then consider y being object such that
A4:
y in dom (p | (Seg n))
and
A5:
(p | (Seg n)) . y = x
by A2, FUNCT_1:def 3;
A6:
dom (p | (Seg n)) = Seg n
by A1, A3, Th35;
then reconsider y = y as Element of NAT by A4;
y <= n
by A4, A6, FINSEQ_1:1;
then A7:
y + 1 <= x .. p
by XREAL_1:19;
y < y + 1
by XREAL_1:29;
then
( dom (p | (Seg n)) c= dom p & y < x .. p )
by A7, RELAT_1:60, XXREAL_0:2;
then
p . y <> x
by A4, Th24;
hence
contradiction
by A4, A5, FUNCT_1:47; verum