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 Def6;
consider b being complex number such that
A2: ( g1 = b & g " = b " ) by Def6;
ex a, b being complex number st
( f " = a & g " = b & (f " ) * (g " ) = a * b ) by A1, A2, Def4;
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, Def4;
hence (f * g) " = (f " ) * (g " ) by A3; :: 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, Def4;
hence (f * g) " = (f " ) * (g " ) by A4; :: 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, Def4;
hence (f * g) " = (f " ) * (g " ) by A5; :: 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, Def4;
hence (f * g) " = (f " ) * (g " ) by A6; :: thesis: verum

end;

end;