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