let G be EVGraph; :: thesis: for e, x being set holds the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x))
let e, x be set ; :: thesis: the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x))
set G2 = G .labelEdge (e,x);

now :: thesis: the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x))

per cases ( e in the_Edges_of G or not e in the_Edges_of G ) ;

suppose e in the_Edges_of G ; :: thesis: the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x))

then G .labelEdge (e,x) = G .set (ELabelSelector,((the_ELabel_of G) +* (e .--> x))) by Def21;
hence the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) by GLIB_000:9; :: thesis: verum

end;

suppose not e in the_Edges_of G ; :: thesis: the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x))

hence the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) by Def21; :: thesis: verum

end;

end;

end;

hence the_VLabel_of G = the_VLabel_of (G .labelEdge (e,x)) ; :: thesis: verum