let f, g be ext-real number ; :: thesis: (f * g) " = (f " ) * (g " )

per cases ( ( f in REAL & g in REAL ) or f = +infty or f = -infty or g = +infty or g = -infty ) by XXREAL_0:14;

suppose ( f in REAL & g in REAL ) ; :: thesis: (f * g) " = (f " ) * (g " )

then reconsider f1 = f, g1 = g as real number ;
consider a being complex number such that
A1: ( f1 = a & f " = a " ) by XXREAL_3:def 4;
consider b being complex number such that
A2: ( g1 = b & g " = b " ) by XXREAL_3:def 4;
ex a, b being complex number st
( f " = a & g " = b & (f " ) * (g " ) = a * b ) by A1, A2, XXREAL_3:def 2;
then (f " ) * (g " ) = (f1 * g1) " by A1, A2, XCMPLX_1:205;
hence (f * g) " = (f " ) * (g " ) ; :: thesis: verum

end;

suppose A3: f = +infty ; :: thesis: (f * g) " = (f " ) * (g " )

( g is positive or g is negative or g = 0 ) ;
then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A3, XXREAL_3:def 2;
hence (f * g) " = (+infty " ) * 0
.= (f " ) * (g " ) by A3, XXREAL_3:1 ;
:: thesis: verum

end;

suppose A4: f = -infty ; :: thesis: (f * g) " = (f " ) * (g " )

( g is positive or g is negative or g = 0 ) ;
then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A4, XXREAL_3:def 2;
hence (f * g) " = (-infty " ) * 0
.= (f " ) * (g " ) by A4, XXREAL_3:1 ;
:: thesis: verum

end;

suppose A5: g = +infty ; :: thesis: (f * g) " = (f " ) * (g " )

( f is positive or f is negative or f = 0 ) ;
then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A5, XXREAL_3:def 2;
hence (f * g) " = 0 * (+infty " )
.= (f " ) * (g " ) by A5, XXREAL_3:1 ;
:: thesis: verum

end;

suppose A6: g = -infty ; :: thesis: (f * g) " = (f " ) * (g " )

( f is positive or f is negative or f = 0 ) ;
then ( (f * g) " = +infty " or (f * g) " = -infty " or (f * g) " = 0 " ) by A6, XXREAL_3:def 2;
hence (f * g) " = 0 * (-infty " )
.= (f " ) * (g " ) by A6, XXREAL_3:1 ;
:: thesis: verum

end;

end;