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 x * (1. Q) = y ;
hence x = y ; :: thesis: verum