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