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
A27: for L being List of X holds L | R1 = union { ((x . O1) \& O2) where x is Element of X : x in L } and
A28: 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 A27
.= L | R2 by A28 ; :: thesis: verum

end;

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