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 that
A1: x in LTLNodes v and
A2: ( 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, Def36
.= chosen_succ (w,v,U,(CastNode (x,v))) by Def16 ;
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 A2, Th59; :: thesis: verum

end;

hence choice_succ_func (w,v,U) is_succ_homomorphism v,w ; :: thesis: verum