let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al holds len (Sgm (seq ((len g),(len f)))) = len f
let f, g be FinSequence of CQC-WFF Al; :: thesis: len (Sgm (seq ((len g),(len f)))) = len f
seq ((len g),(len f)), len f are_equipotent by Th6;
then card (seq ((len g),(len f))) = card (len f) by CARD_1:5;
hence len (Sgm (seq ((len g),(len f)))) = len f by FINSEQ_3:39; :: thesis: verum