let Al be QC-alphabet ; :: thesis: for g, f being FinSequence of CQC-WFF Al holds dom ((g ^ f) | (seq ((len g),(len f)))) = seq ((len g),(len f))
let g, f be FinSequence of CQC-WFF Al; :: 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