set X = v .--> val;
reconsider X = v .--> val as PartFunc of {v},{val} ;
dom (v .--> val) = {v} ;
then reconsider X = X as PartFunc of (the_Vertices_of G),{val} by RELSET_1:5;
rng (v .--> val) = {val} by FUNCOP_1:8;
then reconsider X = X as PartFunc of (the_Vertices_of G),REAL by RELSET_1:6;
G .set (VLabelSelector,X) is real-vlabeled ;
hence G .set (VLabelSelector,(v .--> val)) is [VLabeled] ; :: thesis: verum