let F, G be ext-real-membered set ; :: thesis: for f, g being ext-real number st f in F & g in G holds
f * g in F ** G
let f, g be ext-real number ; :: thesis: ( f in F & g in G implies f * g in F ** G )
( f in ExtREAL & g in ExtREAL ) by XXREAL_0:def 1;
hence ( f in F & g in G implies f * g in F ** G ) ; :: thesis: verum