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