r is right_mult-cancelable by Th11, A1;
hence for b₁, b₂ being Element of R st b₁ * r = 1. R & b₂ * r = 1. R holds
b₁ = b₂ ; :: thesis: verum