set O = No_omega^ 0_No;
A1: 0_No in L_ (No_omega^ 0_No) by Th22;
L_ (No_omega^ 0_No) c= {0_No}

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in L_ (No_omega^ 0_No) or o in {0_No} )
assume A2: ( o in L_ (No_omega^ 0_No) & not o in {0_No} ) ; :: thesis: contradiction
o <> 0_No by A2, TARSKI:def 1;
then ex xL being Surreal ex r being positive Real st
( xL in L_ 0_No & o = (No_omega^ xL) * (uReal . r) ) by A2, Th22;
hence contradiction ; :: thesis: verum

end;

then A3: L_ (No_omega^ 0_No) = {0_No} by A1, ZFMISC_1:33;
R_ (No_omega^ 0_No) = {}

proof

assume R_ (No_omega^ 0_No) <> {} ; :: thesis: contradiction
then consider o being object such that
A4: o in R_ (No_omega^ 0_No) by XBOOLE_0:def 1;
ex xR being Surreal ex r being positive Real st
( xR in R_ 0_No & o = (No_omega^ xR) * (uReal . r) ) by A4, Th23;
hence contradiction ; :: thesis: verum

end;

hence No_omega^ 0_No = 1_No by A3; :: thesis: verum