theorem :: LTLAXIO2:56

for p being Element of LTLB_WFF
for f being FinSequence of LTLB_WFF st ( for i being Nat st i in dom f holds
{} LTLB_WFF |- p => (f /. i) ) holds
{} LTLB_WFF |- p => ((con f) /. (len (con f)))