let R be commutative Ring; :: thesis: for r1 being Element of R st r1 in Unit_Set R holds
r1 is right_mult-cancelable
let r1 be Element of R; :: thesis: ( r1 in Unit_Set R implies r1 is right_mult-cancelable )
assume r1 in Unit_Set R ; :: thesis: r1 is right_mult-cancelable
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

proof

let u, v be Element of R; :: thesis: ( u * r1 = v * r1 implies u = v )
assume u * r1 = v * r1 ; :: thesis: u = v
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: verum

end;

hence r1 is right_mult-cancelable ; :: thesis: verum