let f, g be ExtReal; :: 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 ;
A1: ( ex a being Complex st
( f1 = a & f " = a " ) & ex b being Complex st
( g1 = b & g " = b " ) ) by Def6;
then ex a, b being Complex st
( f " = a & g " = b & (f ") * (g ") = a * b ) by Def5;
then (f ") * (g ") = (f1 * g1) " by A1, XCMPLX_1:204;
hence (f * g) " = (f ") * (g ") ; :: thesis: verum

end;

suppose A2: 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 A2, Def5;
hence (f * g) " = (f ") * (g ") by A2; :: 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, Def5;
hence (f * g) " = (f ") * (g ") by A3; :: thesis: verum

end;

suppose A4: 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 A4, Def5;
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, Def5;
hence (f * g) " = (f ") * (g ") by A5; :: thesis: verum

end;

end;