let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al holds dom (Sgm (seq ((len g),(len f)))) = dom f

let f, g be FinSequence of CQC-WFF Al; :: thesis: dom (Sgm (seq ((len g),(len f)))) = dom f

len (Sgm (seq ((len g),(len f)))) = len f by Th10;

hence dom (Sgm (seq ((len g),(len f)))) = dom f by FINSEQ_3:29; :: thesis: verum

let f, g be FinSequence of CQC-WFF Al; :: thesis: dom (Sgm (seq ((len g),(len f)))) = dom f

len (Sgm (seq ((len g),(len f)))) = len f by Th10;

hence dom (Sgm (seq ((len g),(len f)))) = dom f by FINSEQ_3:29; :: thesis: verum