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 Th45;
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} by FUNCOP_1:19; :: thesis: verum