let p be XFinSequence; :: thesis: for m being Nat st not m in dom p holds
not succ m in dom p
let m be Nat; :: thesis: ( not m in dom p implies not succ m in dom p )
assume not m in dom p ; :: thesis: not succ m in dom p
then A1: m >= card p by Th70;
m + 1 >= m by NAT_1:11;
then m + 1 >= card p by A1, XXREAL_0:2;
hence not succ m in dom p by Th70; :: thesis: verum