let x, y, z be ExtReal; :: thesis: ( x is real & y is real implies x * (y + z) = (x * y) + (x * z) )
assume that
A1: x is real and
A2: y is real ; :: thesis: x * (y + z) = (x * y) + (x * z)
reconsider r = x, s = y as Real by A1, A2;
A3: x * y = r * s ;

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

suppose z in REAL ; :: thesis: x * (y + z) = (x * y) + (x * z)

then reconsider t = z as Real ;
reconsider u = s + t, v = r * s, w = r * t as Real ;
r * u = v + w ;
hence x * (y + z) = (x * y) + (x * z) ; :: thesis: verum

end;

suppose A4: z = -infty ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A5: y + z = -infty by A2, Def2;

per cases ( x is zero or x is positive or x is negative ) ;

suppose x is zero ; :: thesis: x * (y + z) = (x * y) + (x * z)

then x = 0 ;
hence x * (y + z) = (x * y) + (x * z) by Lm26; :: thesis: verum

end;

suppose A6: x is positive ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = -infty by A5, Def5
.= (x * y) + -infty by A3, Def2
.= (x * y) + (x * z) by A4, A6, Def5 ;
:: thesis: verum

end;

suppose A7: x is negative ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = +infty by A5, Def5
.= (x * y) + +infty by A3, Def2
.= (x * y) + (x * z) by A4, A7, Def5 ;
:: thesis: verum

end;

end;

end;

suppose A8: z = +infty ; :: thesis: x * (y + z) = (x * y) + (x * z)

then A9: y + z = +infty by A2, Def2;

per cases ( x is zero or x is positive or x is negative ) ;

suppose x is zero ; :: thesis: x * (y + z) = (x * y) + (x * z)

then x = 0 ;
hence x * (y + z) = (x * y) + (x * z) by Lm26; :: thesis: verum

end;

suppose A10: x is positive ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = +infty by A9, Def5
.= (x * y) + +infty by A3, Def2
.= (x * y) + (x * z) by A8, A10, Def5 ;
:: thesis: verum

end;

suppose A11: x is negative ; :: thesis: x * (y + z) = (x * y) + (x * z)

hence x * (y + z) = -infty by A9, Def5
.= (x * y) + -infty by A3, Def2
.= (x * y) + (x * z) by A8, A11, Def5 ;
:: thesis: verum

end;

end;

end;

end;