assume A1: ( A = F & B = G ) ; :: thesis: A ++ B = F ++ G
let a be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not a in A ++ B or a in F ++ G ) & ( not a in F ++ G or a in A ++ B ) )
hereby :: thesis: ( not a in F ++ G or a in A ++ B )
assume a in A ++ B ; :: thesis: a in F ++ G
then consider c, c1 being Complex such that
A2: a = c + c1 and
A3: ( c in A & c1 in B ) ;
reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, XXREAL_0:def 1;
a = d1 + d2 by A2, A3, XXREAL_3:def 2;
hence a in F ++ G by A1, A3; :: thesis: verum
end;
assume a in F ++ G ; :: thesis: a in A ++ B
then consider w, w1 being Element of ExtREAL such that
A4: a = w + w1 and
A5: ( w in F & w1 in G ) ;
reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A5, XCMPLX_0:def 2;
a = d1 + d2 by A1, A4, A5, XXREAL_3:def 2;
hence a in A ++ B by A1, A5; :: thesis: verum