theorem Th39: :: CALCUL_1:39

for Al being QC-alphabet
for f, g being FinSequence of CQC-WFF Al st Ant f = Ant g & |- f & |- g holds
|- (Ant f) ^ <*((Suc f) '&' (Suc g))*>