theorem Th39: :: PL_AXIOM:51

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