let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
ex f being PVertexMapping of G1,G2 st
( F _V = f & f is isomorphism )
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ex f being PVertexMapping of G1,G2 st
( F _V = f & f is isomorphism ) )
assume A1: F is isomorphism ; :: thesis: ex f being PVertexMapping of G1,G2 st
( F _V = f & f is isomorphism )
then reconsider f = F _V as PVertexMapping of G1,G2 by Th18;
take f ; :: thesis: ( F _V = f & f is isomorphism )
thus F _V = f ; :: thesis: f is isomorphism
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 5 :: thesis: ( f is one-to-one & f is onto & ( for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) ) )
thus f is one-to-one by A1; :: thesis: ( f is onto & ( for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) ) )
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 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
let v, w be Vertex of G1; :: thesis: card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween (((F _V) .: {v}),((F _V) .: {w}))) by A1, GLIB_010:86
.= card (G2 .edgesBetween (((F _V) .: {v}),{((F _V) . w)})) by A2, Lm1
.= card (G2 .edgesBetween ({(f . v)},{(f . w)})) by A2, Lm1 ;
hence card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) ; :: thesis: verum