let phi, psi be Ordinal-Sequence; :: thesis: (phi ^ psi) | (dom phi) = phi
( dom (phi ^ psi) = (dom phi) +^ (dom psi) & ( for A being Ordinal st A in dom phi holds
(phi ^ psi) . A = phi . A ) ) by ORDINAL4:def 1;
then dom phi c= dom (phi ^ psi) by ORDINAL3:27;
then A1: dom phi = (dom (phi ^ psi)) /\ (dom phi) by XBOOLE_1:28;
for x being set 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:68; :: thesis: verum