let x be Surreal; :: thesis: for Inv being Function st Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued holds
( Union (divL (x,Inv)) is surreal-membered & Union (divR (x,Inv)) is surreal-membered )
let Inv be Function; :: thesis: ( Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued implies ( Union (divL (x,Inv)) is surreal-membered & Union (divR (x,Inv)) is surreal-membered ) )
assume A1: Inv is ((L_ x) \/ (R_ x)) \ {0_No} -surreal-valued ; :: thesis: ( Union (divL (x,Inv)) is surreal-membered & Union (divR (x,Inv)) is surreal-membered )
thus Union (divL (x,Inv)) is surreal-membered :: thesis: Union (divR (x,Inv)) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in Union (divL (x,Inv)) or o is surreal )
assume o in Union (divL (x,Inv)) ; :: thesis: o is surreal
then consider n being object such that
A2: ( n in dom (divL (x,Inv)) & o in (divL (x,Inv)) . n ) by CARD_5:2;
dom (divL (x,Inv)) = NAT by Def5;
then reconsider n = n as Nat by A2;
(divL (x,Inv)) . n is surreal-membered by Th9, A1;
hence o is surreal by A2; :: thesis: verum

end;

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in Union (divR (x,Inv)) or o is surreal )
assume o in Union (divR (x,Inv)) ; :: thesis: o is surreal
then consider n being object such that
A3: ( n in dom (divR (x,Inv)) & o in (divR (x,Inv)) . n ) by CARD_5:2;
dom (divR (x,Inv)) = NAT by Def6;
then reconsider n = n as Nat by A3;
(divR (x,Inv)) . n is surreal-membered by Th9, A1;
hence o is surreal by A3; :: thesis: verum