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))) . v = x
let e, x be set ; :: thesis: ( e in the_Vertices_of G implies (the_VLabel_of (G .labelVertex (e,x))) . e = x )
e in {e} by TARSKI:def 1;
then A1: e in dom (e .--> x) ;
assume e in the_Vertices_of G ; :: thesis: (the_VLabel_of (G .labelVertex (e,x))) . e = x
then the_VLabel_of (G .labelVertex (e,x)) = (the_VLabel_of G) +* (e .--> x) by Th38;
then (the_VLabel_of (G .labelVertex (e,x))) . e = (e .--> x) . e by A1, FUNCT_4:13
.= x by FUNCOP_1:72 ;
hence (the_VLabel_of (G .labelVertex (e,x))) . e = x ; :: thesis: verum