let p be FinSequence; :: thesis: for x being object st x in rng p holds
not x in rng (p -| x)
let x be object ; :: 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, 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; :: thesis: verum