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

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