let O be Operation of X; :: thesis: ( O = O2 | iff for L being List of X holds L | O = (L | O1) | O2 )
thus ( O = O2 | implies for L being List of X holds L | O = (L | O1) | O2 ) by RELAT_1:126; :: thesis: ( ( for L being List of X holds L | O = (L | O1) | O2 ) implies O = O2 | )
assume A22: for L being List of X holds L | O = (L | O1) | O2 ; :: thesis: O = O2 |

now :: thesis: for L being List of X holds L | O = L | (O1 * O2)

let L be List of X; :: thesis: L | O = L | (O1 * O2)
thus L | O = (L | O1) | O2 by A22
.= L | (O1 * O2) by RELAT_1:126 ; :: thesis: verum

end;

hence O = O2 | by Th30; :: thesis: verum