let Q be multLoop; :: thesis: for x, y, z, u being Element of Q st x * y = u & x * z = u holds
y = z
let x, y, z, u be Element of Q; :: thesis: ( x * y = u & x * z = u implies y = z )
assume ( x * y = u & x * z = u ) ; :: thesis: y = z
then x \ (x * y) = x \ (x * z) ;
hence y = z ; :: thesis: verum