let L be non degenerated doubleLoopStr ; :: thesis: ( L is Field-like & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable implies ( L is commutative & L is associative & L is well-unital & L is almost_left_invertible ) )
assume A1: ( L is Field-like & L is Abelian & L is distributive & L is add-associative & L is right_zeroed & L is right_complementable ) ; :: thesis: ( L is commutative & L is associative & L is well-unital & L is almost_left_invertible )
then for x, y being Element of L holds x * y = y * x by Th20;
hence L is commutative by GROUP_1:def 12; :: thesis: ( L is associative & L is well-unital & L is almost_left_invertible )
for x, y, z being Element of L holds (x * y) * z = x * (y * z) by A1, Th19;
hence L is associative by GROUP_1:def 3; :: thesis: ( L is well-unital & L is almost_left_invertible )
for x being Element of L holds
( x * (1. L) = x & (1. L) * x = x ) by A1, Th21;
hence L is well-unital ; :: thesis: L is almost_left_invertible
let x be Element of L; :: according to ALGSTR_0:def 38 :: thesis: ( x = 0. L or x is left_invertible )
assume x <> 0. L ; :: thesis: x is left_invertible
then not x in {(0. L)} by TARSKI:def 1;
then reconsider x = x as Element of NonZero L by XBOOLE_0:def 5;
consider y being Element of NonZero L such that
x * y = 1. L and
A2: y * x = 1. L by A1, Th7;
take y ; :: according to ALGSTR_0:def 27 :: thesis: y * x = 1. L
thus y * x = 1. L by A2; :: thesis: verum