let x, y, z be ext-real number ; :: 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 pc: not x in REAL ;
assume C: not x * (y * z) = (x * y) * z ; :: thesis: contradiction
then ppc: ( y <> 0 & z <> 0 ) by LmZ, LmZ1;

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

suppose S: 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 ppc;

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

then -infty * (y * z) = -infty by Def4
.= -infty * z by A, Def4
.= (-infty * y) * z by A, Def4 ;
hence contradiction by S, C; :: thesis: verum

end;

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

then -infty * (y * z) = +infty by Def4
.= -infty * z by A, Def4
.= (-infty * y) * z by A, Def4 ;
hence contradiction by S, C; :: thesis: verum

end;

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

then -infty * (y * z) = +infty by Def4
.= +infty * z by A, Def4
.= (-infty * y) * z by A, Def4 ;
hence contradiction by S, C; :: thesis: verum

end;

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

then -infty * (y * z) = -infty by Def4
.= +infty * z by A, Def4
.= (-infty * y) * z by A, Def4 ;
hence contradiction by S, C; :: thesis: verum

end;

end;

end;

suppose S: 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 ppc;

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

then +infty * (y * z) = +infty by Def4
.= +infty * z by A, Def4
.= (+infty * y) * z by A, Def4 ;
hence contradiction by S, C; :: thesis: verum

end;

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

then +infty * (y * z) = -infty by Def4
.= +infty * z by A, Def4
.= (+infty * y) * z by A, Def4 ;
hence contradiction by S, C; :: thesis: verum

end;

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

then +infty * (y * z) = -infty by Def4
.= -infty * z by A, Def4
.= (+infty * y) * z by A, Def4 ;
hence contradiction by S, C; :: thesis: verum

end;

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

then +infty * (y * z) = +infty by Def4
.= -infty * z by A, Def4
.= (+infty * y) * z by A, Def4 ;
hence contradiction by S, C; :: thesis: verum

end;

end;

end;

end;