let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is Disomorphism ) )
assume A1: G1 == G2 ; :: thesis: ex F being PGraphMapping of G1,G2 st
( F = id G1 & F is Disomorphism )
then reconsider F = id G1 as PGraphMapping of G1,G2 by GLIB_010:11;
take F ; :: thesis: ( F = id G1 & F is Disomorphism )
thus F = id G1 ; :: thesis: F is Disomorphism
( dom (F _V) = the_Vertices_of G1 & dom (F _E) = the_Edges_of G1 ) ;
then A2: F is total by GLIB_010:def 11;
( rng (F _V) = the_Vertices_of G2 & rng (F _E) = the_Edges_of G2 ) by A1, GLIB_000:def 34;
then A3: F is onto by GLIB_010:def 12;
( F _V is one-to-one & F _E is one-to-one ) ;
then A4: F is one-to-one by GLIB_010:def 13;

now :: thesis: for e, v, w being object st e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 holds
(F _E) . e DJoins (F _V) . v,(F _V) . w,G2

let e, v, w be object ; :: thesis: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) & e DJoins v,w,G1 implies (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )
assume A5: ( e in dom (F _E) & v in dom (F _V) & w in dom (F _V) ) ; :: thesis: ( e DJoins v,w,G1 implies (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 )
assume e DJoins v,w,G1 ; :: thesis: (F _E) . e DJoins (F _V) . v,(F _V) . w,G2
then ((id G1) _E) . e DJoins ((id G1) _V) . v,((id G1) _V) . w,G1 by A5, GLIB_010:def 14;
hence (F _E) . e DJoins (F _V) . v,(F _V) . w,G2 by A1, GLIB_000:88; :: thesis: verum

end;

then F is directed by GLIB_010:def 14;
hence F is Disomorphism by A2, A3, A4; :: thesis: verum