let R be commutative Ring; :: thesis:
let r1 be Element of R; :: thesis:
assume r1 in Unit_Set R ; :: thesis:
then consider r2 being Element of R such that
A2: r2 * r1 = 1. R by Th10;
for u, v being Element of R st u * r1 = v * r1 holds
u = v

let u, v be Element of R; :: thesis:
assume u * r1 = v * r1 ; :: thesis:
then A5: r1 * (u - v) = (r1 * v) - (r1 * v) by VECTSP_1:11
.= 0. R by RLVECT_1:15 ;
u - v = (r2 * r1) * (u - v) by A2
.= r2 * (r1 * (u - v)) by GROUP_1:def 3
.= 0. R by A5 ;
hence u = v by VECTSP_1:19; :: thesis:

end;