let n be non zero Nat; :: thesis: RN_Base n <> {}
0 + 1 <= n by NAT_1:13;
then Base_FinSeq n,1 in { (Base_FinSeq n,i) where i is Element of NAT : ( 1 <= i & i <= n ) } ;
hence RN_Base n <> {} ; :: thesis: verum