let p be XFinSequence; :: thesis: p is initial
let m, n be Nat; :: according to AFINSQ_1:def 12 :: thesis: ( n in dom p & m < n implies m in dom p )
assume A1: n in dom p ; :: thesis: ( not m < n or m in dom p )
assume m < n ; :: thesis: m in dom p
then m in Segm n by NAT_1:44;
hence m in dom p by A1, ORDINAL1:10; :: thesis: verum