let phi, psi be Ordinal-Sequence; :: thesis: (phi ^ psi) | (dom phi) = phi
dom (phi ^ psi) = (dom phi) +^ (dom psi) by ORDINAL4:def 1;
then dom phi c= dom (phi ^ psi) by ORDINAL3:24;
then A1: dom phi = (dom (phi ^ psi)) /\ (dom phi) by XBOOLE_1:28;
for x being object st x in dom phi holds
phi . x = (phi ^ psi) . x by ORDINAL4:def 1;
hence (phi ^ psi) | (dom phi) = phi by A1, FUNCT_1:46; :: thesis: verum