theorem Th40: :: LTLAXIO1:40

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