let Q be multLoop; :: thesis: for x being Element of Q holds x \ x = 1. Q
let x be Element of Q; :: thesis: x \ x = 1. Q
x * (1. Q) = x ;
hence x \ x = 1. Q ; :: thesis: verum