let F, G be ext-real-membered set ; :: thesis: for f, g being ExtReal st f in F & g in G holds
f + g in F ++ G
let f, g be ExtReal; :: thesis: ( f in F & g in G implies f + g in F ++ G )
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def 1;
hence ( f in F & g in G implies f + g in F ++ G ) ; :: thesis: verum