let I be non degenerated commutative domRing-like Ring; :: thesis: ( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable )
A1: the_Field_of_Quotients I is add-associative

proof

for u, v, w being Element of the carrier of (the_Field_of_Quotients I) holds (u + v) + w = u + (v + w) by Th22;
hence the_Field_of_Quotients I is add-associative by RLVECT_1:def 6; :: thesis: verum

end;

A2: the_Field_of_Quotients I is right_zeroed

proof

for v being Element of (the_Field_of_Quotients I) holds v + (0. (the_Field_of_Quotients I)) = v by Th24;
hence the_Field_of_Quotients I is right_zeroed by RLVECT_1:def 7; :: thesis: verum

end;

the_Field_of_Quotients I is right_complementable

proof

let v be Element of (the_Field_of_Quotients I); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider m = v as Element of Quot. I ;
reconsider n = (quotaddinv I) . m as Element of (the_Field_of_Quotients I) ;
take w = n; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. (the_Field_of_Quotients I)
thus v + w = 0. (the_Field_of_Quotients I) by Th30; :: thesis: verum

end;

hence ( the_Field_of_Quotients I is add-associative & the_Field_of_Quotients I is right_zeroed & the_Field_of_Quotients I is right_complementable ) by A1, A2; :: thesis: verum