let p be FinSequence; :: thesis: for x being object
for n being Nat st x in rng p & n = (x .. p) - 1 holds
p | (Seg n) = p -| x
let x be object ; :: thesis: for n being Nat st x in rng p & n = (x .. p) - 1 holds
p | (Seg n) = p -| x
let n be Nat; :: thesis: ( x in rng p & n = (x .. p) - 1 implies p | (Seg n) = p -| x )
assume x in rng p ; :: thesis: ( not n = (x .. p) - 1 or p | (Seg n) = p -| x )
then ex m being Nat st
( m = (x .. p) - 1 & p | (Seg m) = p -| x ) by Def5;
hence ( not n = (x .. p) - 1 or p | (Seg n) = p -| x ) ; :: thesis: verum