let F, G, H be ext-real-membered set ; :: thesis: F ++ (G \/ H) = (F ++ G) \/ (F ++ H)
let j be ExtReal; :: according to MEMBERED:def 14 :: thesis: ( ( not j in F ++ (G \/ H) or j in (F ++ G) \/ (F ++ H) ) & ( not j in (F ++ G) \/ (F ++ H) or j in F ++ (G \/ H) ) )

hereby :: thesis: ( not j in (F ++ G) \/ (F ++ H) or j in F ++ (G \/ H) )

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

end;

assume A4: j in (F ++ G) \/ (F ++ H) ; :: thesis: j in F ++ (G \/ H)

per cases ( j in F ++ G or j in F ++ H ) by A4, XBOOLE_0:def 3;

suppose j in F ++ G ; :: thesis: j in F ++ (G \/ H)

then consider w, w1 being Element of ExtREAL such that
A5: ( j = w + w1 & w in F ) and
A6: w1 in G ;
w1 in G \/ H by A6, XBOOLE_0:def 3;
hence j in F ++ (G \/ H) by A5; :: thesis: verum

end;

suppose j in F ++ H ; :: thesis: j in F ++ (G \/ H)

then consider w, w1 being Element of ExtREAL such that
A7: ( j = w + w1 & w in F ) and
A8: w1 in H ;
w1 in G \/ H by A8, XBOOLE_0:def 3;
hence j in F ++ (G \/ H) by A7; :: thesis: verum

end;

end;