let M be non empty commutative multLoopStr_0 ; :: thesis: ( M is almost_left_invertible implies M is almost_right_invertible )
assume A6: M is almost_left_invertible ; :: thesis: M is almost_right_invertible
let x be Element of M; :: according to ALGSTR_0:def 39 :: thesis: ( x = 0. M or x is right_invertible )
assume x <> 0. M ; :: thesis: x is right_invertible
then consider y being Element of M such that
A7: y * x = 1. M by A6;
take y ; :: according to ALGSTR_0:def 28 :: thesis: x * y = 1. M
thus x * y = 1. M by A7; :: thesis: verum