let R be non degenerated commutative domRing-like Ring; :: thesis: for a being Element of R holds a / (1. R) = a
let a be Element of R; :: thesis: a / (1. R) = a
set A = a / (1. R);
(1. R) * a = a ;
then A1: ( 1. R <> 0. R & 1. R divides a ) ;
a / (1. R) = (a / (1. R)) * (1. R)
.= a by A1, Def4 ;
hence a / (1. R) = a ; :: thesis: verum