let p be FinSequence; :: thesis: for x being object st x in rng p holds
len (p -| x) = (x .. p) - 1
let x be object ; :: thesis: ( x in rng p implies len (p -| x) = (x .. p) - 1 )
assume A1: x in rng p ; :: thesis: len (p -| x) = (x .. p) - 1
then consider n being Nat such that
A2: n = (x .. p) - 1 and
A3: p | (Seg n) = p -| x by Def5;
A4: n <= n + 1 by NAT_1:12;
n + 1 <= len p by A1, A2, Th21;
then n <= len p by A4, XXREAL_0:2;
hence len (p -| x) = (x .. p) - 1 by A2, A3, FINSEQ_1:17; :: thesis: verum