let v be LTL-formula; :: thesis: 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
let w be Element of Inf_seq AtomicFamily; :: thesis: for f being Function of (LTLNodes v),(LTLNodes v) st f is_succ_homomorphism v,w holds
f is_homomorphism v,w
set LN = LTLNodes v;
let f be Function of (LTLNodes v),(LTLNodes v); :: thesis: ( f is_succ_homomorphism v,w implies f is_homomorphism v,w )
assume f is_succ_homomorphism v,w ; :: thesis: f is_homomorphism v,w
then for y being set st y in LTLNodes v & not CastNode (y,v) is elementary & w |= * (CastNode (y,v)) holds
w |= * (CastNode ((f . y),v)) by Def32;
hence f is_homomorphism v,w by Def33; :: thesis: verum