theorem Th17: :: LTLAXIO2:17

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