take Polynom-Ring the Field ; :: thesis: not Polynom-Ring the Field is almost_left_invertible
thus not Polynom-Ring the Field is almost_left_invertible by lemr; :: thesis: verum