deffunc H1( set ) -> strict LTLnode over v = chosen_succ (w,v,U,(CastNode ($1,v)));
A1:
for x being set st x in LTLNodes v holds
H1(x) in LTLNodes v
by Def30;
consider IT being Function of (LTLNodes v),(LTLNodes v) such that
A2:
for x being set st x in LTLNodes v holds
IT . x = H1(x)
from FUNCT_2:sch 11(A1);
take
IT
; for x being set st x in LTLNodes v holds
IT . x = chosen_succ (w,v,U,(CastNode (x,v)))
thus
for x being set st x in LTLNodes v holds
IT . x = chosen_succ (w,v,U,(CastNode (x,v)))
by A2; verum