let o be object ; :: thesis: for x being Surreal holds
( o in L_ (No_omega^ x) iff ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ) )
let x be Surreal; :: thesis: ( o in L_ (No_omega^ x) iff ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ) )
thus ( not o in L_ (No_omega^ x) or o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ) :: thesis: ( ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ) implies o in L_ (No_omega^ x) )

proof

assume ( o in L_ (No_omega^ x) & not o = 0_No ) ; :: thesis: ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) )
then consider xL being Surreal, r being positive Real such that
A1: ( xL in L_ x & o = (No_omega^ xL) *' (uReal . r) ) by Lm4;
o = (No_omega^ xL) * (uReal . r) by A1;
hence ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) by A1; :: thesis: verum

end;

assume ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ) ; :: thesis: o in L_ (No_omega^ x)

per cases then ( o = 0_No or ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ) ;

suppose o = 0_No ; :: thesis: o in L_ (No_omega^ x)

hence o in L_ (No_omega^ x) by Lm4; :: thesis: verum

end;

suppose ex xL being Surreal ex r being positive Real st
( xL in L_ x & o = (No_omega^ xL) * (uReal . r) ) ; :: thesis: o in L_ (No_omega^ x)

hence o in L_ (No_omega^ x) by Lm4; :: thesis: verum

end;

end;