let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is Disomorphism holds
ex f being directed PVertexMapping of G1,G2 st
( F _V = f & f is Disomorphism )
let F be PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism implies ex f being directed PVertexMapping of G1,G2 st
( F _V = f & f is Disomorphism ) )
assume A1: F is Disomorphism ; :: thesis: ex f being directed PVertexMapping of G1,G2 st
( F _V = f & f is Disomorphism )
then reconsider f = F _V as directed PVertexMapping of G1,G2 by Th21;
take f ; :: thesis: ( F _V = f & f is Disomorphism )
thus F _V = f ; :: thesis: f is Disomorphism
A2: dom f = the_Vertices_of G1 by A1, GLIB_010:def 11;
hence f is total by PARTFUN1:def 2; :: according to GLIB_011:def 6 :: thesis: ( f is one-to-one & f is onto & ( for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) ) ) )
thus f is one-to-one by A1; :: thesis: ( f is onto & ( for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) ) ) )
rng f = the_Vertices_of G2 by A1, GLIB_010:def 12;
hence f is onto by FUNCT_2:def 3; :: thesis: for v, w being Vertex of G1 holds
( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) )
let v, w be Vertex of G1; :: thesis: ( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) )
A3: card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween (((F _V) .: {v}),((F _V) .: {w}))) by A1, GLIB_010:88
.= card (G2 .edgesDBetween (((F _V) .: {v}),{((F _V) . w)})) by A2, Lm1
.= card (G2 .edgesDBetween ({(f . v)},{(f . w)})) by A2, Lm1 ;
card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween (((F _V) .: {w}),((F _V) .: {v}))) by A1, GLIB_010:88
.= card (G2 .edgesDBetween (((F _V) .: {w}),{((F _V) . v)})) by A2, Lm1
.= card (G2 .edgesDBetween ({(f . w)},{(f . v)})) by A2, Lm1 ;
hence ( card (G1 .edgesDBetween ({v},{w})) = card (G2 .edgesDBetween ({(f . v)},{(f . w)})) & card (G1 .edgesDBetween ({w},{v})) = card (G2 .edgesDBetween ({(f . w)},{(f . v)})) ) by A3; :: thesis: verum