u divides 1. R by GCD_1:def 2;
then consider a being Element of R such that
H1: u * a = 1. R ;
v divides 1. R by GCD_1:def 2;
then consider b being Element of R such that
H2: v * b = 1. R ;
(b * a) * (u * v) = b * (a * (u * v)) by GROUP_1:def 3
.= b * ((a * u) * v) by GROUP_1:def 3
.= 1. R by H2, H1 ;
then u * v divides 1. R ;
hence u * v is unital ; :: thesis: verum