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:31; :: thesis: verum