theorem :: LTLAXIO2:18

for n being Element of NAT
for f being FinSequence of LTLB_WFF
for g being Function of LTLB_WFF,BOOLEAN st n in dom f holds
(VAL g) . ((con f) /. (len (con f))) = (((VAL g) . ((con (f | (n -' 1))) /. (len (con (f | (n -' 1)))))) '&' ((VAL g) . (f /. n))) '&' ((VAL g) . ((con (f /^ n)) /. (len (con (f /^ n)))))