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 object st x in LTLNodes v holds
f1 . x = f2 . x
proof
let x be object ; :: 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:12; :: thesis: verum