reconsider X = v .--> val as PartFunc of {v},{val} ;
dom (v .--> val) = {v} by FUNCOP_1:19;
then reconsider X = X as PartFunc of (the_Vertices_of G),{val} by RELSET_1:13;
for x being set st x in {val} holds
x in REAL by XREAL_0:def 1;
then {val} c= REAL by TARSKI:def 3;
then reconsider X = X as PartFunc of (the_Vertices_of G),REAL by RELSET_1:17;
G .set VLabelSelector ,X is real-vlabeled ;
hence G .set VLabelSelector ,(v .--> val) is real-vlabeled ; :: thesis: verum