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