let I be non degenerated commutative domRing-like Ring; :: thesis: the_Field_of_Quotients I is well-unital
let x be Element of (the_Field_of_Quotients I); :: according to VECTSP_1:def 16 :: thesis: ( x * (1. (the_Field_of_Quotients I)) = x & (1. (the_Field_of_Quotients I)) * x = x )
thus ( x * (1. (the_Field_of_Quotients I)) = x & (1. (the_Field_of_Quotients I)) * x = x ) by Th27; :: thesis: verum