let F, G be ext-real-membered set ; :: thesis: for r being Real holds r ++ (F /\ G) = (r ++ F) /\ (r ++ G)
let r be Real; :: thesis: r ++ (F /\ G) = (r ++ F) /\ (r ++ G)
A1: (r ++ F) /\ (r ++ G) c= r ++ (F /\ G)

proof

let j be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not j in (r ++ F) /\ (r ++ G) or j in r ++ (F /\ G) )
assume A2: j in (r ++ F) /\ (r ++ G) ; :: thesis: j in r ++ (F /\ G)
then j in r ++ F by XBOOLE_0:def 4;
then consider w being Element of ExtREAL such that
A3: j = r + w and
A4: w in F by Th134;
j in r ++ G by A2, XBOOLE_0:def 4;
then consider w1 being Element of ExtREAL such that
A5: j = r + w1 and
A6: w1 in G by Th134;
w = w1 by A3, A5, XXREAL_3:11;
then w in F /\ G by A4, A6, XBOOLE_0:def 4;
hence j in r ++ (F /\ G) by A3, Th132; :: thesis: verum

end;

r ++ (F /\ G) c= (r ++ F) /\ (r ++ G) by Th42;
hence r ++ (F /\ G) = (r ++ F) /\ (r ++ G) by A1; :: thesis: verum