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