let O1, O2 be Operation of X; ( ( for L being List of X holds L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) & ( for L being List of X holds L | O2 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } ) implies O1 = O2 )
assume that
A8:
for L being List of X holds L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
and
A9:
for L being List of X holds L | O2 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L }
; O1 = O2
now for L being List of X holds L | O1 = L | O2end;
hence
O1 = O2
by Th30; verum