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 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 n ; :: according to ALGSTR_0:def 11 :: thesis: v + n = 0. (the_Field_of_Quotients I)
thus v + n = 0. (the_Field_of_Quotients I) by Th28; :: thesis: verum

end;

( ( for u, v, w being Element of (the_Field_of_Quotients I) holds (u + v) + w = u + (v + w) ) & ( for v being Element of (the_Field_of_Quotients I) holds v + (0. (the_Field_of_Quotients I)) = v ) ) by Th20, Th22;
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, RLVECT_1:def 3, RLVECT_1:def 4; :: thesis: verum