let F, G be ext-real-membered set ; :: thesis: (F \/ G) "" = (F "" ) \/ (G "" )
let i be ext-real number ; :: according to MEMBERED:def 14 :: thesis: ( ( not i in (F \/ G) "" or i in (F "" ) \/ (G "" ) ) & ( not i in (F "" ) \/ (G "" ) or i in (F \/ G) "" ) )

hereby :: thesis: ( not i in (F "" ) \/ (G "" ) or i in (F \/ G) "" )

assume i in (F \/ G) "" ; :: thesis: i in (F "" ) \/ (G "" )
then consider w being Element of ExtREAL such that
A1: i = w " and
A2: w in F \/ G ;
( w in F or w in G ) by A2, XBOOLE_0:def 3;
then ( w " in F "" or w " in G "" ) ;
hence i in (F "" ) \/ (G "" ) by A1, XBOOLE_0:def 3; :: thesis: verum

end;

assume A3: i in (F "" ) \/ (G "" ) ; :: thesis: i in (F \/ G) ""

per cases ( i in F "" or i in G "" ) by A3, XBOOLE_0:def 3;

suppose i in F "" ; :: thesis: i in (F \/ G) ""

then consider w being Element of ExtREAL such that
A4: i = w " and
A5: w in F ;
w in F \/ G by A5, XBOOLE_0:def 3;
hence i in (F \/ G) "" by A4; :: thesis: verum

end;

suppose i in G "" ; :: thesis: i in (F \/ G) ""

then consider w being Element of ExtREAL such that
A6: i = w " and
A7: w in G ;
w in F \/ G by A7, XBOOLE_0:def 3;
hence i in (F \/ G) "" by A6; :: thesis: verum

end;

end;