set G0 = G .set (ELabelSelector,X);
VLabelSelector in dom G
by Def2;
then
VLabelSelector in (dom G) \/ {ELabelSelector}
by XBOOLE_0:def 3;
hence
VLabelSelector in dom (G .set (ELabelSelector,X))
by GLIB_000:7; GLIB_010:def 2 ex f being ManySortedSet of the_Vertices_of (G .set (ELabelSelector,X)) st (G .set (ELabelSelector,X)) . VLabelSelector = f
consider f being ManySortedSet of the_Vertices_of G such that
A2:
G . VLabelSelector = f
by Def2;
G == G .set (ELabelSelector,X)
by GLIB_003:7;
then
the_Vertices_of G = the_Vertices_of (G .set (ELabelSelector,X))
by GLIB_000:def 34;
then reconsider f = f as ManySortedSet of the_Vertices_of (G .set (ELabelSelector,X)) ;
take
f
; (G .set (ELabelSelector,X)) . VLabelSelector = f
ELabelSelector <> VLabelSelector
by GLIB_003:def 3, GLIB_003:def 2;
hence
(G .set (ELabelSelector,X)) . VLabelSelector = f
by A2, GLIB_000:9; verum