deffunc H₁( set ) -> strict LTLnode over 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 11(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