theorem Th13: :: CALCUL_2:13

for Al being QC-alphabet
for i being Element of NAT
for f, g being FinSequence of CQC-WFF Al st i in dom (Sgm (seq ((len g),(len f)))) holds
(Sgm (seq ((len g),(len f)))) . i = (len g) + i