deffunc H₁( set ) -> strict LTLnode of v = chosen_succ w,v,U,(CastNode $1,v);
A1: for x being set st x in LTLNodes v holds
H₁(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 = H₁(x) from FUNCT_2:sch 2(A1);
take IT ; :: thesis: 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; :: thesis: verum