let I be non degenerated commutative domRing-like Ring; the_Field_of_Quotients I is non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative distributive doubleLoopStr
A1:
the_Field_of_Quotients I is almost_left_invertible
A3:
( q0. I <> q1. I & 0. (the_Field_of_Quotients I) = q0. I )
by Th19;
A4:
( 1. (the_Field_of_Quotients I) = q1. I & ( for x, y, z being Element of (the_Field_of_Quotients I) holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) ) )
by Th26, Th27;
( ( for x, y, z being Element of (the_Field_of_Quotients I) holds (x * y) * z = x * (y * z) ) & ( for u, v being Element of (the_Field_of_Quotients I) holds u + v = v + u ) )
by Th21, Th23;
hence
the_Field_of_Quotients I is non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed unital associative distributive doubleLoopStr
by A1, A3, A4, GROUP_1:def 3, RLVECT_1:def 2, STRUCT_0:def 8, VECTSP_1:def 7; verum