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