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

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

hence
R1 = R2
by Th30; :: thesis: verumlet 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;thus L | R1 = union { ((x . O1) \& O2) where x is Element of X : x in L } by A27

.= L | R2 by A28 ; :: thesis: verum