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

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