assume not RN_Base 0 is empty ; :: thesis: contradiction
then consider x being object 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