set G0 = G .set (VLabelSelector,X);

ELabelSelector in dom G by Def1;

then ELabelSelector in (dom G) \/ {VLabelSelector} by XBOOLE_0:def 3;

hence ELabelSelector in dom (G .set (VLabelSelector,X)) by GLIB_000:7; :: according to GLIB_010:def 1 :: thesis: ex f being ManySortedSet of the_Edges_of (G .set (VLabelSelector,X)) st (G .set (VLabelSelector,X)) . ELabelSelector = f

consider f being ManySortedSet of the_Edges_of G such that

A2: G . ELabelSelector = f by Def1;

G == G .set (VLabelSelector,X) by GLIB_003:7;

then the_Edges_of G = the_Edges_of (G .set (VLabelSelector,X)) by GLIB_000:def 34;

then reconsider f = f as ManySortedSet of the_Edges_of (G .set (VLabelSelector,X)) ;

take f ; :: thesis: (G .set (VLabelSelector,X)) . ELabelSelector = f

VLabelSelector <> ELabelSelector by GLIB_003:def 3, GLIB_003:def 2;

hence (G .set (VLabelSelector,X)) . ELabelSelector = f by A2, GLIB_000:9; :: thesis: verum

ELabelSelector in dom G by Def1;

then ELabelSelector in (dom G) \/ {VLabelSelector} by XBOOLE_0:def 3;

hence ELabelSelector in dom (G .set (VLabelSelector,X)) by GLIB_000:7; :: according to GLIB_010:def 1 :: thesis: ex f being ManySortedSet of the_Edges_of (G .set (VLabelSelector,X)) st (G .set (VLabelSelector,X)) . ELabelSelector = f

consider f being ManySortedSet of the_Edges_of G such that

A2: G . ELabelSelector = f by Def1;

G == G .set (VLabelSelector,X) by GLIB_003:7;

then the_Edges_of G = the_Edges_of (G .set (VLabelSelector,X)) by GLIB_000:def 34;

then reconsider f = f as ManySortedSet of the_Edges_of (G .set (VLabelSelector,X)) ;

take f ; :: thesis: (G .set (VLabelSelector,X)) . ELabelSelector = f

VLabelSelector <> ELabelSelector by GLIB_003:def 3, GLIB_003:def 2;

hence (G .set (VLabelSelector,X)) . ELabelSelector = f by A2, GLIB_000:9; :: thesis: verum