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);
A1: 1. R <> 0. R ;
(1. R) * a = a by VECTSP_1:def 19;
then A2: 1. R divides a by Def1;
a / (1. R) = (a / (1. R)) * (1. R) by VECTSP_1:def 13
.= a by A1, A2, Def4 ;
hence a / (1. R) = a ; :: thesis: verum