theorem Th25: :: GOEDELCP:25

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