theorem Th13: :: CALCUL_2:13

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