theorem Th36: :: MODELC_3:36

for k being Nat
for L being FinSequence
for v being LTL-formula st L is_Finseq_for v & 1 <= k & k <= len L holds
len (CastNode ((L . k),v)) <= ((len (CastNode ((L . 1),v))) - k) + 1