let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of (the_Field_of_Quotients I) holds - u = (quotaddinv I) . u
let u be Element of (the_Field_of_Quotients I); :: thesis: - u = (quotaddinv I) . u
reconsider z = (quotaddinv I) . u as Element of (the_Field_of_Quotients I) by Th32;
z + u = 0. (the_Field_of_Quotients I) by Th28;
hence - u = (quotaddinv I) . u by RLVECT_1:6; :: thesis: verum