let x, y, z be ext-real number ; :: thesis: ( x is real & not y is real implies x * (y + z) = (x * y) + (x * z) )
assume that
Z1: x is real and
Z2: not y is real ; :: thesis: x * (y + z) = (x * y) + (x * z)

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

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

hence x * (y + z) = (x * y) + (x * z) by Z1, Lm12A; :: thesis: verum

end;

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

then pc: ( not y in REAL & not z in REAL ) by Z2;

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

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

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

end;

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

hence x * (y + z) = (x * y) + (x * z) by Th11, Tx4A; :: thesis: verum

end;

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

hence x * (y + z) = (x * y) + (x * z) by Th11, Tx4B; :: thesis: verum

end;

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

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

end;

end;

end;

end;