theorem Th40: :: PL_AXIOM:52

for p being Element of PL-WFF
for F being Subset of PL-WFF
for f, f1 being FinSequence of PL-WFF st f = f1 ^ <*p*> & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
prc f1,F,i ) & prc f,F, len f holds
( ( for i being Nat st 1 <= i & i <= len f holds
prc f,F,i ) & F |- p )