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