for v being LTL-formula
for w being Element of Inf_seq AtomicFamily
for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
f is_homomorphism v,w ;