let f1, f2 be Function of (LTLNodes v),(LTLNodes v); :: thesis: ( ( 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) ; :: thesis: f1 = f2
for x being set st x in LTLNodes v holds
f1 . x = f2 . x

proof

let x be set ; :: thesis: ( x in LTLNodes v implies f1 . x = f2 . x )
assume A5: x in LTLNodes v ; :: thesis: f1 . x = f2 . x
then f1 . x = chosen_succ w,v,U,(CastNode x,v) by A3
.= f2 . x by A4, A5 ;
hence f1 . x = f2 . x ; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:18; :: thesis: verum