let G1, G2 be plain _Graph; :: thesis:
dom G1 = _GraphSelectors by Def1;
then A1: dom G1 = dom G2 by Def1;
assume A2: G1 == G2 ; :: thesis:
for x being object st x in dom G1 holds
G1 . x = G2 . x

let x be object ; :: thesis:
assume x in dom G1 ; :: thesis:
then x in _GraphSelectors by Def1;

per cases by ENUMSET1:def 2, GLIB_000:def 5;

suppose A3: x = VertexSelector ; :: thesis:

hence G1 . x = the_Vertices_of G1 by GLIB_000:def 6
.= the_Vertices_of G2 by A2, GLIB_000:def 34
.= G2 . x by A3, GLIB_000:def 6 ;
:: thesis:

end;

suppose A4: x = EdgeSelector ; :: thesis:

hence G1 . x = the_Edges_of G1 by GLIB_000:def 7
.= the_Edges_of G2 by A2, GLIB_000:def 34
.= G2 . x by A4, GLIB_000:def 7 ;
:: thesis:

end;

suppose A5: x = SourceSelector ; :: thesis:

thus G1 . x = the_Source_of G1 by A5, GLIB_000:def 8
.= the_Source_of G2 by A2, GLIB_000:def 34
.= G2 . x by A5, GLIB_000:def 8 ; :: thesis:

end;

suppose A6: x = TargetSelector ; :: thesis:

hence G1 . x = the_Target_of G1 by GLIB_000:def 9
.= the_Target_of G2 by A2, GLIB_000:def 34
.= G2 . x by A6, GLIB_000:def 9 ;
:: thesis:

end;

end;

end;

hence G1 = G2 by A1, FUNCT_1:2; :: thesis: