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

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

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

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

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

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

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

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

end;

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

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

end;

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

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

end;

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

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

end;

end;

end;

end;