let f, g be ExtReal; :: 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 w1, w2 being Element of ExtREAL such that
A1: i = w1 * w2 and
A2: ( w1 in {f} & w2 in {g} ) ;
( w1 = f & w2 = g ) by A2, TARSKI:def 1;
hence i in {(f * g)} by A1, TARSKI:def 1; :: thesis: verum

end;

A3: ( f in {f} & g in {g} ) by TARSKI:def 1;
assume i in {(f * g)} ; :: thesis: i in {f} ** {g}
then A4: i = f * g by TARSKI:def 1;
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def 1;
hence i in {f} ** {g} by A4, A3; :: thesis: verum