let R be domRing; :: thesis: not Polynom-Ring R is almost_left_invertible
set PR = Polynom-Ring R;
reconsider p = rpoly (2,(0. R)) as Element of the carrier of (Polynom-Ring R) by POLYNOM3:def 10;
A3: p <> 0. (Polynom-Ring R) by POLYNOM3:def 10;
now :: thesis: for q being Element of (Polynom-Ring R) holds not q * p = 1. (Polynom-Ring R)
assume ex q being Element of (Polynom-Ring R) st q * p = 1. (Polynom-Ring R) ; :: thesis: contradiction
then consider q being Element of (Polynom-Ring R) such that
A1: q * p = 1. (Polynom-Ring R) ;
A9: q <> 0. (Polynom-Ring R) by A1;
reconsider q = q as Element of the carrier of (Polynom-Ring R) ;
A4: q <> 0_. R by A9, POLYNOM3:def 10;
then A5: deg q is Element of NAT by T8b;
q *' p = 1. (Polynom-Ring R) by A1, POLYNOM3:def 10
.= 1_. R by POLYNOM3:def 10 ;
then A2: (deg q) + (deg p) = deg (1_. R) by A4, HURWITZ:23;
A8: len (1_. R) = 1 by POLYNOM4:4;
deg p = 2 by HURWITZ:27;
hence contradiction by A5, A8, A2; :: thesis: verum
end;
then not p is left_invertible ;
hence not Polynom-Ring R is almost_left_invertible by A3; :: thesis: verum