let x, y, z be ext-real number ; :: thesis: ( x is real & y is real implies x * (y + z) = (x * y) + (x * z) )
assume Z: ( x is real & y is real ) ; :: thesis: x * (y + z) = (x * y) + (x * z)
then reconsider r = x, s = y as real number ;
V: 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 number ;
reconsider u = s + t, v = r * s, w = r * t as real number ;
r * u = v + w ;
hence x * (y + z) = (x * y) + (x * z) ; :: thesis: verum

end;

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

then T: y + z = -infty by Def3, Z;

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)

hence x * (y + z) = (x * y) + (x * z) by LmY; :: thesis: verum

end;

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

hence x * (y + z) = -infty by T, Def4
.= (x * y) + -infty by V, Def3
.= (x * y) + (x * z) by SS, S, Def4 ;
:: thesis: verum

end;

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

hence x * (y + z) = +infty by T, Def4
.= (x * y) + +infty by V, Def3
.= (x * y) + (x * z) by SS, S, Def4 ;
:: thesis: verum

end;

end;

end;

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

then T: y + z = +infty by Def3, Z;

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)

hence x * (y + z) = (x * y) + (x * z) by LmY; :: thesis: verum

end;

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

hence x * (y + z) = +infty by T, Def4
.= (x * y) + +infty by V, Def3
.= (x * y) + (x * z) by SS, S, Def4 ;
:: thesis: verum

end;

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

hence x * (y + z) = -infty by T, Def4
.= (x * y) + -infty by V, Def3
.= (x * y) + (x * z) by SS, S, Def4 ;
:: thesis: verum

end;

end;

end;

end;