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

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:12; :: 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