let R1, R2 be Operation of X; :: thesis: ( ( for L being List of X holds L | R1 = union { ((x . O1) \& O2) where x is Element of X : x in L } ) & ( for L being List of X holds L | R2 = union { ((x . O1) \& O2) where x is Element of X : x in L } ) implies R1 = R2 )
assume that
A1: for L being List of X holds L | R1 = union { ((x . O1) \& O2) where x is Element of X : x in L } and
A2: for L being List of X holds L | R2 = union { ((x . O1) \& O2) where x is Element of X : x in L } ; :: thesis: R1 = R2

now :: thesis: for L being List of X holds L | R1 = L | R2

let L be List of X; :: thesis: L | R1 = L | R2
thus L | R1 = union { ((x . O1) \& O2) where x is Element of X : x in L } by A1
.= L | R2 by A2 ; :: thesis: verum

end;

hence R1 = R2 by Th3; :: thesis: verum