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