let G1, G2 be _finite _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is strong_SG-embedding & G1 .order() = G2 .order() & G1 .size() = G2 .size() holds
F is isomorphism
let F be PGraphMapping of G1,G2; :: thesis: ( F is strong_SG-embedding & G1 .order() = G2 .order() & G1 .size() = G2 .size() implies F is isomorphism )
assume that
A1: F is strong_SG-embedding and
A2: ( G1 .order() = G2 .order() & G1 .size() = G2 .size() ) ; :: thesis: F is isomorphism
A3: card (rng (F _V)) = card (dom (F _V)) by A1, CARD_1:70
.= card (the_Vertices_of G1) by A1, Def11
.= G2 .order() by A2, GLIB_000:def 24
.= card (the_Vertices_of G2) by GLIB_000:def 24 ;
card (rng (F _E)) = card (dom (F _E)) by A1, CARD_1:70
.= card (the_Edges_of G1) by A1, Def11
.= G2 .size() by A2, GLIB_000:def 25
.= card (the_Edges_of G2) by GLIB_000:def 25 ;
then F is onto by A3, CARD_2:102;
hence F is isomorphism by A1; :: thesis: verum