let R be commutative domRing-like Ring; :: thesis: for a being Element of R st a <> 0. R holds
a / a = 1. R
let A be Element of R; :: thesis: ( A <> 0. R implies A / A = 1. R )
assume A1: A <> 0. R ; :: thesis: A / A = 1. R
then (A / A) * A = A by Def4
.= (1. R) * A ;
hence A / A = 1. R by A1, Th1; :: thesis: verum