consider F being Field;
F is Ring ;
hence ex b₁ being Ring st
( not b₁ is degenerated & b₁ is almost_left_invertible ) ; :: thesis: verum