let x, y, z be ExtReal; :: thesis: ( not y is real implies x * (y * z) = (x * y) * z )
assume not y is real ; :: thesis: x * (y * z) = (x * y) * z
then A1: not y in REAL ;
assume A2: not x * (y * z) = (x * y) * z ; :: thesis: contradiction
then A3: ( x <> 0 & z <> 0 ) by Lm19;

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

suppose A4: y = -infty ; :: thesis: contradiction

per cases ( ( x is positive & z is positive ) or ( x is positive & z is negative ) or ( x is negative & z is positive ) or ( x is negative & z is negative ) ) by A3;

suppose A5: ( x is positive & z is positive ) ; :: thesis: contradiction

then x * (-infty * z) = x * -infty by Def5
.= -infty by A5, Def5
.= -infty * z by A5, Def5
.= (x * -infty) * z by A5, Def5 ;
hence contradiction by A2, A4; :: thesis: verum

end;

suppose A6: ( x is positive & z is negative ) ; :: thesis: contradiction

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

end;

suppose A7: ( x is negative & z is positive ) ; :: thesis: contradiction

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

end;

suppose A8: ( x is negative & z is negative ) ; :: thesis: contradiction

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

end;

end;

end;

suppose A9: y = +infty ; :: thesis: contradiction

per cases ( ( x is positive & z is positive ) or ( x is positive & z is negative ) or ( x is negative & z is positive ) or ( x is negative & z is negative ) ) by A3;

suppose A10: ( x is positive & z is positive ) ; :: thesis: contradiction

then x * (+infty * z) = x * +infty by Def5
.= +infty by A10, Def5
.= +infty * z by A10, Def5
.= (x * +infty) * z by A10, Def5 ;
hence contradiction by A2, A9; :: thesis: verum

end;

suppose A11: ( x is positive & z is negative ) ; :: thesis: contradiction

then x * (+infty * z) = x * -infty by Def5
.= -infty by A11, Def5
.= +infty * z by A11, Def5
.= (x * +infty) * z by A11, Def5 ;
hence contradiction by A2, A9; :: thesis: verum

end;

suppose A12: ( x is negative & z is positive ) ; :: thesis: contradiction

then x * (+infty * z) = x * +infty by Def5
.= -infty by A12, Def5
.= -infty * z by A12, Def5
.= (x * +infty) * z by A12, Def5 ;
hence contradiction by A2, A9; :: thesis: verum

end;

suppose A13: ( x is negative & z is negative ) ; :: thesis: contradiction

then x * (+infty * z) = x * -infty by Def5
.= +infty by A13, Def5
.= -infty * z by A13, Def5
.= (x * +infty) * z by A13, Def5 ;
hence contradiction by A2, A9; :: thesis: verum

end;

end;

end;

end;