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 |

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)

hence
O = O2 |
by Th30; :: thesis: verumlet 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;thus L | O = (L | O1) | O2 by A22

.= L | (O1 * O2) by RELAT_1:126 ; :: thesis: verum