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:90;
hence dom ((g ^ f) | (seq (len g),(len f))) = seq (len g),(len f) by Th14, XBOOLE_1:28; :: thesis: verum