now :: thesis: G .labelVertex (v,x) is real-vlabeled

per cases ( v in the_Vertices_of G or not v in the_Vertices_of G ) ;

suppose A1: v in the_Vertices_of G ; :: thesis: G .labelVertex (v,x) is real-vlabeled

reconsider x = x as Element of REAL by XREAL_0:def 1;
set EL = (the_VLabel_of G) +* (v .--> x);
rng (the_VLabel_of G) c= REAL ;
then the_VLabel_of G is PartFunc of (dom (the_VLabel_of G)),REAL by RELSET_1:4;
then the_VLabel_of G is PartFunc of (the_Vertices_of G),REAL by Lm2, RELSET_1:5;
then reconsider EL = (the_VLabel_of G) +* (v .--> x) as PartFunc of (the_Vertices_of G),REAL by A1, Lm4;
G .labelVertex (v,x) = G .set (VLabelSelector,EL) by A1, Def22;
hence G .labelVertex (v,x) is real-vlabeled ; :: thesis: verum

end;

suppose not v in the_Vertices_of G ; :: thesis: G .labelVertex (v,x) is real-vlabeled

hence G .labelVertex (v,x) is real-vlabeled by Def22; :: thesis: verum

end;

end;

end;

hence G .labelVertex (v,x) is real-vlabeled ; :: thesis: verum