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

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

hence
O1 = O2
by Th30; :: thesis: verumlet 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;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