let f, g be ExtReal; :: thesis: {f} ++ {g} = {(f + g)}
let j be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not j in {f} ++ {g} or j in {(f + g)} ) & ( not j in {(f + g)} or j in {f} ++ {g} ) )
hereby :: thesis: ( not j in {(f + g)} or j in {f} ++ {g} )
assume j in {f} ++ {g} ; :: thesis: j in {(f + g)}
then consider w1, w2 being Element of ExtREAL such that
A1: j = w1 + w2 and
A2: ( w1 in {f} & w2 in {g} ) ;
( w1 = f & w2 = g ) by A2, TARSKI:def 1;
hence j in {(f + g)} by A1, TARSKI:def 1; :: thesis: verum
end;
A3: ( f in {f} & g in {g} ) by TARSKI:def 1;
assume j in {(f + g)} ; :: thesis: j in {f} ++ {g}
then A4: j = f + g by TARSKI:def 1;
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def 1;
hence j in {f} ++ {g} by A4, A3; :: thesis: verum