let g, f be FinSequence of CQC-WFF ; :: thesis: len (Sgm (seq (len g),(len f))) = len f
seq (len g),(len f), len f are_equipotent by Th6;
then A1: card (seq (len g),(len f)) = card (len f) by CARD_1:21;
seq (len g),(len f) c= Seg ((len g) + (len f)) by Th7;
hence len (Sgm (seq (len g),(len f))) = len f by A1, FINSEQ_3:44; :: thesis: verum