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 )
assume e in the_Vertices_of G ; :: thesis: (the_VLabel_of (G .labelVertex e,x)) . e = x
then A1: the_VLabel_of (G .labelVertex e,x) = (the_VLabel_of G) +* (e .--> x) by Th45;
e in {e} by TARSKI:def 1;
then e in dom (e .--> x) by FUNCOP_1:19;
then (the_VLabel_of (G .labelVertex e,x)) . e = (e .--> x) . e by A1, FUNCT_4:14
.= x by FUNCOP_1:87 ;
hence (the_VLabel_of (G .labelVertex e,x)) . e = x ; :: thesis: verum