theorem Th12: :: CARD_5:12

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