let p be FinSequence; :: thesis: for x being set st x in rng p holds
not x in rng (p -| x)
let x be set ; :: thesis: ( 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) ; :: thesis: contradiction
reconsider n = (x .. p) - 1 as Element of NAT by A1, Th32;
set r = p | (Seg n);
A3: p | (Seg n) = p -| x by A1, Th45;
then consider y being set such that
A4: y in dom (p | (Seg n)) and
A5: (p | (Seg n)) . y = x by A2, FUNCT_1:def 5;
A6: dom (p | (Seg n)) = Seg n by A1, A3, Th47;
then reconsider y = y as Element of NAT by A4;
y <= n by A4, A6, FINSEQ_1:3;
then A7: y + 1 <= x .. p by XREAL_1:21;
y < y + 1 by XREAL_1:31;
then ( dom (p | (Seg n)) c= dom p & y < x .. p ) by A7, RELAT_1:89, XXREAL_0:2;
then p . y <> x by A4, Th34;
hence contradiction by A4, A5, FUNCT_1:70; :: thesis: verum