let F, G, H be ext-real-membered set ; :: thesis: F ** (G /\ H) c= (F ** G) /\ (F ** H)
let j be ExtReal; :: according to MEMBERED:def 8 :: thesis: ( not j in F ** (G /\ H) or j in (F ** G) /\ (F ** 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 H by A3, XBOOLE_0:def 4;
then A4: w * w1 in F ** H by A2;
w1 in G by A3, XBOOLE_0:def 4;
then w * w1 in F ** G by A2;
hence j in (F ** G) /\ (F ** H) by A1, A4, XBOOLE_0:def 4; :: thesis: verum