let g, f be FinSequence of CQC-WFF ; :: 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