let p be FinSequence; :: thesis: for x being object
for n being Nat st x in rng p & n = (x .. p) - 1 holds
dom (p -| x) = Seg n
let x be object ; :: thesis: for n being Nat st x in rng p & n = (x .. p) - 1 holds
dom (p -| x) = Seg n
let n be Nat; :: thesis: ( x in rng p & n = (x .. p) - 1 implies dom (p -| x) = Seg n )
assume x in rng p ; :: thesis: ( not n = (x .. p) - 1 or dom (p -| x) = Seg n )
then len (p -| x) = (x .. p) - 1 by Th34;
hence ( not n = (x .. p) - 1 or dom (p -| x) = Seg n ) by FINSEQ_1:def 3; :: thesis: verum