let Q be multLoop; 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; ( a_op (x,y,z) = 1. Q implies L_map (z,y,x) = z )
assume
a_op (x,y,z) = 1. Q
; 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
; verum