let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of (the_Field_of_Quotients I) st u <> 0. (the_Field_of_Quotients I) holds
ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I)
let u be Element of (the_Field_of_Quotients I); :: thesis: ( u <> 0. (the_Field_of_Quotients I) implies ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I) )
assume A1: u <> 0. (the_Field_of_Quotients I) ; :: thesis: ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I)
reconsider u = u as Element of Quot. I ;
reconsider v = (quotmultinv I) . u as Element of (the_Field_of_Quotients I) ;
reconsider u = u as Element of (the_Field_of_Quotients I) ;
u * v = 1. (the_Field_of_Quotients I) by A1, Th29;
hence ex v being Element of (the_Field_of_Quotients I) st u * v = 1. (the_Field_of_Quotients I) ; :: thesis: verum