let F, G be ext-real-membered set ; :: thesis: (F ** G) "" = (F "" ) ** (G "" )
let i be ext-real number ; :: according to MEMBERED:def 14 :: thesis: ( ( not i in (F ** G) "" or i in (F "" ) ** (G "" ) ) & ( not i in (F "" ) ** (G "" ) or i in (F ** G) "" ) )

hereby :: thesis: ( not i in (F "" ) ** (G "" ) or i in (F ** G) "" )

assume i in (F ** G) "" ; :: thesis: i in (F "" ) ** (G "" )
then consider w being Element of ExtREAL such that
A1: i = w " and
A2: w in F ** G ;
consider w1, w2 being Element of ExtREAL such that
A3: w = w1 * w2 and
A4: w1 in F and
A5: w2 in G by A2;
A6: i = (w1 " ) * (w2 " ) by A1, A3, Th2;
( w1 " in F "" & w2 " in G "" ) by A4, A5;
hence i in (F "" ) ** (G "" ) by A6, Th85; :: thesis: verum

end;

assume i in (F "" ) ** (G "" ) ; :: thesis: i in (F ** G) ""
then consider w, w1 being Element of ExtREAL such that
A7: i = w * w1 and
A8: w in F "" and
A9: w1 in G "" ;
consider w2 being Element of ExtREAL such that
A10: w = w2 " and
A11: w2 in F by A8;
consider w3 being Element of ExtREAL such that
A12: w1 = w3 " and
A13: w3 in G by A9;
A14: w2 * w3 in F ** G by A11, A13;
i = (w2 * w3) " by A7, A10, A12, Th2;
hence i in (F ** G) "" by A14; :: thesis: verum