theorem :: ZF_FUND1:25

for o, p, q, r, s, t being set st p <> r holds
{[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} by Lm15;