theorem Th12: :: CALCUL_2:12

for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al holds rng (Sgm (seq ((len g),(len f)))) = seq ((len g),(len f)) by FINSEQ_1:def 14;