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