let G1, G2 be plain _Graph; :: thesis: ( G1 == G2 implies G1 = G2 )

dom G1 = _GraphSelectors by Def1;

then A1: dom G1 = dom G2 by Def1;

assume A2: G1 == G2 ; :: thesis: G1 = G2

for x being object st x in dom G1 holds

G1 . x = G2 . x

dom G1 = _GraphSelectors by Def1;

then A1: dom G1 = dom G2 by Def1;

assume A2: G1 == G2 ; :: thesis: G1 = G2

for x being object st x in dom G1 holds

G1 . x = G2 . x

proof

hence
G1 = G2
by A1, FUNCT_1:2; :: thesis: verum
let x be object ; :: thesis: ( x in dom G1 implies G1 . x = G2 . x )

assume x in dom G1 ; :: thesis: G1 . x = G2 . x

then x in _GraphSelectors by Def1;

end;assume x in dom G1 ; :: thesis: G1 . x = G2 . x

then x in _GraphSelectors by Def1;

per cases then
( x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector )
by ENUMSET1:def 2, GLIB_000:def 5;

end;

suppose A3:
x = VertexSelector
; :: thesis: G1 . x = G2 . x

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: verum

end;.= the_Vertices_of G2 by A2, GLIB_000:def 34

.= G2 . x by A3, GLIB_000:def 6 ;

:: thesis: verum

suppose A4:
x = EdgeSelector
; :: thesis: G1 . x = G2 . x

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: verum

end;.= the_Edges_of G2 by A2, GLIB_000:def 34

.= G2 . x by A4, GLIB_000:def 7 ;

:: thesis: verum

suppose A5:
x = SourceSelector
; :: thesis: G1 . x = G2 . x

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: verum

end;.= the_Source_of G2 by A2, GLIB_000:def 34

.= G2 . x by A5, GLIB_000:def 8 ; :: thesis: verum

suppose A6:
x = TargetSelector
; :: thesis: G1 . x = G2 . x

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: verum

end;.= the_Target_of G2 by A2, GLIB_000:def 34

.= G2 . x by A6, GLIB_000:def 9 ;

:: thesis: verum