let y, z, x be ext-real number ; :: thesis: ( y >= 0 & z >= 0 implies x * (y + z) = (x * y) + (x * z) )
assume Z: ( 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 Z;

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

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

end;

suppose T: ( 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 Th106; :: thesis: verum

end;

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

then pc: not x in REAL ;

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

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

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

end;

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

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

end;

end;

end;

end;

end;

end;