let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al holds rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f))

let f, g be FinSequence of CQC-WFF Al; :: 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

let f, g be FinSequence of CQC-WFF Al; :: 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