let f1, f2 be Function of (LTLNodes v),(LTLNodes v); ( ( for x being set st x in LTLNodes v holds
f1 . x = chosen_succ (w,v,U,(CastNode (x,v))) ) & ( for x being set st x in LTLNodes v holds
f2 . x = chosen_succ (w,v,U,(CastNode (x,v))) ) implies f1 = f2 )
assume that
A3:
for x being set st x in LTLNodes v holds
f1 . x = chosen_succ (w,v,U,(CastNode (x,v)))
and
A4:
for x being set st x in LTLNodes v holds
f2 . x = chosen_succ (w,v,U,(CastNode (x,v)))
; f1 = f2
for x being object st x in LTLNodes v holds
f1 . x = f2 . x
hence
f1 = f2
by FUNCT_2:12; verum