let O1, O2 be Operation of X; :: thesis: ( ( 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 } ; :: thesis: O1 = O2
now :: thesis: for L being List of X holds L | O1 = L | O2
let L be List of X; :: thesis: L | O1 = L | O2
thus L | O1 = union { (IFEQ ((x . O),{},{x},{})) where x is Element of X : x in L } by A8
.= L | O2 by A9 ; :: thesis: verum
end;
hence O1 = O2 by Th30; :: thesis: verum