let G be VGraph; :: thesis: for v, x being set st v in the_Vertices_of G holds
(G .labelVertex (v,x)) .labeledV() = (G .labeledV()) \/ {v}
let e, val be set ; :: thesis: ( e in the_Vertices_of G implies (G .labelVertex (e,val)) .labeledV() = (G .labeledV()) \/ {e} )
set G2 = G .labelVertex (e,val);
set EG = the_VLabel_of G;
set EG2 = the_VLabel_of (G .labelVertex (e,val));
assume e in the_Vertices_of G ; :: thesis: (G .labelVertex (e,val)) .labeledV() = (G .labeledV()) \/ {e}
then the_VLabel_of (G .labelVertex (e,val)) = (the_VLabel_of G) +* (e .--> val) by Th38;
then dom (the_VLabel_of (G .labelVertex (e,val))) = (dom (the_VLabel_of G)) \/ (dom (e .--> val)) by FUNCT_4:def 1;
hence (G .labelVertex (e,val)) .labeledV() = (G .labeledV()) \/ {e} ; :: thesis: verum