let x be R_eal; :: thesis: ( ( x = +infty or x = -infty ) implies for y being R_eal holds x * y <> 1 )
assume A1: ( x = +infty or x = -infty ) ; :: thesis: for y being R_eal holds x * y <> 1
given y being R_eal such that A2: x * y = 1 ; :: thesis: contradiction

per cases ( y = 0 or 0 < y or y < 0 ) ;

suppose y = 0 ; :: thesis: contradiction

hence contradiction by A2, EXTREAL1:def 1; :: thesis: verum

end;

suppose A3: 0 < y ; :: thesis: contradiction

now

per cases ( x = +infty or x = -infty ) by A1;

suppose x = +infty ; :: thesis: contradiction

hence contradiction by A2, A3, EXTREAL1:def 1; :: thesis: verum

end;

suppose x = -infty ; :: thesis: contradiction

hence contradiction by A2, A3, EXTREAL1:def 1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose A4: y < 0 ; :: thesis: contradiction

now

per cases ( x = +infty or x = -infty ) by A1;

suppose x = +infty ; :: thesis: contradiction

hence contradiction by A2, A4, EXTREAL1:def 1; :: thesis: verum

end;

suppose x = -infty ; :: thesis: contradiction

hence contradiction by A2, A4, EXTREAL1:def 1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

end;