assume not RN_Base 0 is empty ; :: thesis: contradiction
then consider x being set such that
A1: x in RN_Base 0 by XBOOLE_0:def 1;
ex i being Element of NAT st
( x = Base_FinSeq 0 ,i & 1 <= i & i <= 0 ) by A1;
hence contradiction ; :: thesis: verum