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;
A7: dom (p | (Seg n)) c= dom p by RELAT_1:89;
y <= n by A4, A6, FINSEQ_1:3;
then ( y + 1 <= x .. p & y < y + 1 ) by XREAL_1:21, XREAL_1:31;
then y < x .. p by XXREAL_0:2;
then p . y <> x by A4, A7, Th34;
hence contradiction by A4, A5, FUNCT_1:70; :: thesis: verum