assume j in F ** (G \/ H) ; :: thesis:
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:

end;

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

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:

end;

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:

end;