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 defSuccHom;
hence f is_homomorphism v,w by defHom; :: thesis: verum