let M be non empty commutative multLoopStr_0 ; :: thesis: ( M is almost_right_invertible implies M is almost_left_invertible )
assume A8: M is almost_right_invertible ; :: thesis: M is almost_left_invertible
let x be Element of M; :: according to VECTSP_1:def 9 :: thesis: ( x = 0. M or ex b₁ being Element of the carrier of M st b₁ * x = 1. M )
assume x <> 0. M ; :: thesis: ex b₁ being Element of the carrier of M st b₁ * x = 1. M
then consider y being Element of M such that
A9: x * y = 1. M by A8, ALGSTR_0:def 28;
take y ; :: thesis: y * x = 1. M
thus y * x = 1. M by A9; :: thesis: verum