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