let g, f be FinSequence of CQC-WFF ; :: thesis: dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f))
dom ((g ^ f) | (seq ((len g),(len f)))) = (dom (g ^ f)) /\ (seq ((len g),(len f))) by RELAT_1:61;
hence dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f)) by Th14, XBOOLE_1:28; :: thesis: verum