assume A1: ( A = F & B = G ) ; :: thesis: A ++ B = F ++ G
let a be ext-real number ; :: 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 Element of COMPLEX such that
A2: a = c + c1 and
A3: c in A and
A4: c1 in B ;
reconsider d1 = c, d2 = c1 as Element of ExtREAL by A3, A4, XXREAL_0:def 1;
a = d1 + d2 by A2, A3, A4, XXREAL_3:def 2;
hence a in F ++ G by A1, A3, A4; :: thesis: verum

end;

assume a in F ++ G ; :: thesis: a in A ++ B
then consider w, w1 being Element of ExtREAL such that
A5: a = w + w1 and
A6: w in F and
A7: w1 in G ;
reconsider d1 = w, d2 = w1 as Element of COMPLEX by A1, A6, A7, XCMPLX_0:def 2;
a = d1 + d2 by A1, A7, A5, A6, XXREAL_3:def 2;
hence a in A ++ B by A1, A6, A7; :: thesis: verum