theorem :: LTLAXIO2:21

for f, f1 being FinSequence of LTLB_WFF
for g being Function of LTLB_WFF,BOOLEAN st rng f = rng f1 holds
(VAL g) . ((con f) /. (len (con f))) = (VAL g) . ((con f1) /. (len (con f1)))