let x be Element of K; :: thesis: ( not x is zero implies x is right_mult-cancelable )
assume not x is zero ; :: thesis: x is right_mult-cancelable
then x is left_invertible ;
then consider x1 being Element of K such that
A3: x1 * x = 1. K by ALGSTR_0:def 27;

now :: thesis: for y, z being Element of K st y * x = z * x holds
y = z

let y, z be Element of K; :: thesis: ( y * x = z * x implies y = z )
assume A4: y * x = z * x ; :: thesis: y = z
thus y = y * (1. K)
.= (z * x) * x1 by A3, A4, GROUP_1:def 3
.= z * (1. K) by A3, GROUP_1:def 3
.= z ; :: thesis: verum

end;

hence x is right_mult-cancelable by ALGSTR_0:def 21; :: thesis: verum