let F, G be ext-real-membered set ; :: thesis: (F ** G) "" = (F "") ** (G "")
let i be ExtReal; :: 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 & w2 in G ) by A2;
A5: ( w1 " in F "" & w2 " in G "" ) by A4;
i = (w1 ") * (w2 ") by A1, A3, XXREAL_3:67;
hence i in (F "") ** (G "") by A5; :: thesis: verum
end;
assume i in (F "") ** (G "") ; :: thesis: i in (F ** G) ""
then consider w, w1 being Element of ExtREAL such that
A6: i = w * w1 and
A7: w in F "" and
A8: w1 in G "" ;
consider w3 being Element of ExtREAL such that
A9: w1 = w3 " and
A10: w3 in G by A8;
consider w2 being Element of ExtREAL such that
A11: w = w2 " and
A12: w2 in F by A7;
A13: w2 * w3 in F ** G by A12, A10;
i = (w2 * w3) " by A6, A11, A9, XXREAL_3:67;
hence i in (F ** G) "" by A13; :: thesis: verum