theorem Th8: :: MODELC_3:8

for L1, L2 being FinSequence
for H being LTL-formula
for W being Subset of (Subformulae H) st rng L1 = Subformulae H & L1 is one-to-one & rng L2 = Subformulae H & L2 is one-to-one holds
len (L1,W) = len (L2,W)