let v be LTL-formula; :: thesis: for w being Element of Inf_seq AtomicFamily
for U being Choice_Function of BOOL (Subformulae v) holds choice_succ_func w,v,U is_succ_homomorphism v,w
let w be Element of Inf_seq AtomicFamily ; :: thesis: for U being Choice_Function of BOOL (Subformulae v) holds choice_succ_func w,v,U is_succ_homomorphism v,w
let U be Choice_Function of BOOL (Subformulae v); :: thesis: choice_succ_func w,v,U is_succ_homomorphism v,w
set f = choice_succ_func w,v,U;
for x being set st x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) holds
( CastNode ((choice_succ_func w,v,U) . x),v is_succ_of CastNode x,v & w |= * (CastNode ((choice_succ_func w,v,U) . x),v) )

proof

let x be set ; :: thesis: ( x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) implies ( CastNode ((choice_succ_func w,v,U) . x),v is_succ_of CastNode x,v & w |= * (CastNode ((choice_succ_func w,v,U) . x),v) ) )
assume A1: ( x in LTLNodes v & not CastNode x,v is elementary & w |= * (CastNode x,v) ) ; :: thesis: ( CastNode ((choice_succ_func w,v,U) . x),v is_succ_of CastNode x,v & w |= * (CastNode ((choice_succ_func w,v,U) . x),v) )
set N = CastNode x,v;
set SN = chosen_succ w,v,U,(CastNode x,v);
CastNode ((choice_succ_func w,v,U) . x),v = CastNode (chosen_succ w,v,U,(CastNode x,v)),v by A1, Defchoicesuccfunc
.= chosen_succ w,v,U,(CastNode x,v) by defCastNode01 ;
hence ( CastNode ((choice_succ_func w,v,U) . x),v is_succ_of CastNode x,v & w |= * (CastNode ((choice_succ_func w,v,U) . x),v) ) by A1, Thchosensucc01; :: thesis: verum

end;

hence choice_succ_func w,v,U is_succ_homomorphism v,w by defSuccHom; :: thesis: verum