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