let g, f be FinSequence of CQC-WFF ; :: thesis: rng (Sgm (seq (len g),(len f))) = seq (len g),(len f)
seq (len g),(len f) c= Seg ((len g) + (len f)) by Th7;
hence rng (Sgm (seq (len g),(len f))) = seq (len g),(len f) by FINSEQ_1:def 13; :: thesis: verum