let x, y, z be ExtReal; :: thesis: ( y >= 0 & z >= 0 implies x * (y + z) = (x * y) + (x * z) )
assume A1: ( y >= 0 & z >= 0 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

per cases ( y = 0 or z = 0 or ( y > 0 & z > 0 ) ) by A1;

suppose ( y = 0 or z = 0 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

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

end;

suppose A2: ( y > 0 & z > 0 ) ; :: thesis: x * (y + z) = (x * y) + (x * z)

per cases ( x is real or not x is real ) ;

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

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

end;

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

then A3: not x in REAL ;

per cases ( x = -infty or x = +infty ) by A3, XXREAL_0:14;

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

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

end;

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

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

end;

end;

end;

end;

end;

end;