let G be VGraph; :: thesis: for v, x being set st v in the_Vertices_of G holds
the_VLabel_of (G .labelVertex (v,x)) = (the_VLabel_of G) +* (v .--> x)
let e, x be set ; :: thesis: ( e in the_Vertices_of G implies the_VLabel_of (G .labelVertex (e,x)) = (the_VLabel_of G) +* (e .--> x) )
assume e in the_Vertices_of G ; :: thesis: the_VLabel_of (G .labelVertex (e,x)) = (the_VLabel_of G) +* (e .--> x)
then the_VLabel_of (G .labelVertex (e,x)) = (G .set (VLabelSelector,((the_VLabel_of G) +* (e .--> x)))) . VLabelSelector by Def22;
hence the_VLabel_of (G .labelVertex (e,x)) = (the_VLabel_of G) +* (e .--> x) by GLIB_000:8; :: thesis: verum