let I be non degenerated commutative domRing-like Ring; :: thesis: 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 associative

proof

for x, y, z being Element of the carrier of (the_Field_of_Quotients I) holds (x * y) * z = x * (y * z) by Th25;
hence the_Field_of_Quotients I is associative by GROUP_1:def 4; :: thesis: verum

end;

A2: the_Field_of_Quotients I is almost_left_invertible

proof

let x be Element of (the_Field_of_Quotients I); :: according to ALGSTR_0:def 39 :: thesis: ( x = 0. (the_Field_of_Quotients I) or x is left_invertible )
assume x <> 0. (the_Field_of_Quotients I) ; :: thesis: x is left_invertible
then consider y being Element of (the_Field_of_Quotients I) such that
A3: x * y = 1. (the_Field_of_Quotients I) by Th48;
take y ; :: according to ALGSTR_0:def 27 :: thesis: y * x = 1. (the_Field_of_Quotients I)
thus y * x = 1. (the_Field_of_Quotients I) by A3; :: thesis: verum

end;

A4: the_Field_of_Quotients I is Abelian

proof

for u, v being Element of (the_Field_of_Quotients I) holds u + v = v + u by Th23;
hence the_Field_of_Quotients I is Abelian by RLVECT_1:def 5; :: thesis: verum

end;

A5: not the_Field_of_Quotients I is degenerated

proof

A6: q0. I <> q1. I by Th21;
A7: 0. (the_Field_of_Quotients I) = q0. I ;
1. (the_Field_of_Quotients I) = q1. I ;
hence not the_Field_of_Quotients I is degenerated by A6, A7, STRUCT_0:def 8; :: thesis: verum

end;

the_Field_of_Quotients I is distributive

proof

for x, y, z being Element of the carrier of (the_Field_of_Quotients I) holds
( x * (y + z) = (x * y) + (x * z) & (y + z) * x = (y * x) + (z * x) ) by Th28, Th29;
hence the_Field_of_Quotients I is distributive by VECTSP_1:def 18; :: thesis: verum

end;

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, A2, A4, A5; :: thesis: verum