let G be EVGraph; :: thesis: for v, x being set holds the_ELabel_of G = the_ELabel_of (G .labelVertex (v,x))
let e, x be set ; :: thesis: the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x))
set G2 = G .labelVertex (e,x);

now :: thesis: the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x))

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

suppose e in the_Vertices_of G ; :: thesis: the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x))

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

end;

suppose not e in the_Vertices_of G ; :: thesis: the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x))

hence the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x)) by Def22; :: thesis: verum

end;

end;

end;

hence the_ELabel_of G = the_ELabel_of (G .labelVertex (e,x)) ; :: thesis: verum