theorem Th39: :: LTLAXIO5:27

for X being Subset of LTLB_WFF
for f, f1, f2 being FinSequence of LTLB_WFF st f2 = f ^ f1 & 1 <= len f & 1 <= len f1 & ( for i being Nat st 1 <= i & i <= len f holds
prc0 f,X,i ) & ( for i being Nat st 1 <= i & i <= len f1 holds
prc0 f1,X,i ) holds
for i being Nat st 1 <= i & i <= len f2 holds
prc0 f2,X,i