set R = INT.Ring ;
set a = (1. INT.Ring) + (1. INT.Ring);
now :: thesis: for y being Element of INT.Ring holds not y * ((1. INT.Ring) + (1. INT.Ring)) = 1. INT.Ring
assume ex y being Element of INT.Ring st y * ((1. INT.Ring) + (1. INT.Ring)) = 1. INT.Ring ; :: thesis: contradiction
then consider y being Element of INT.Ring such that
A1: y * ((1. INT.Ring) + (1. INT.Ring)) = 1. INT.Ring ;
reconsider i = y as Integer ;
consider k being Nat such that
A2: ( k = 1 * (2 ") or - k = 1 * (2 ") ) by A1, INT_1:def 1;
thus contradiction by A2, NAT_1:14; :: thesis: verum
end;
then not (1. INT.Ring) + (1. INT.Ring) is left_invertible ;
hence not INT.Ring is almost_left_invertible ; :: thesis: verum