for phi, psi being Ordinal-Sequence holds (phi ^ psi) | (dom phi) = phi