let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
G1 .numComponents() = G2 .numComponents()
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies G1 .numComponents() = G2 .numComponents() )
set S = { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } ;
assume A1: F is isomorphism ; :: thesis: G1 .numComponents() = G2 .numComponents()
A2: G1 .componentSet() is non empty Subset of (bool (dom (F _V))) by A1, GLIB_010:def 11;
A3: (.: (F _V)) | (G1 .componentSet()) is one-to-one by A1, FUNCT_1:52;
A4: rng ((.: (F _V)) | (G1 .componentSet())) = { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } by A1, A2, Th6;
A5: dom ((.: (F _V)) | (G1 .componentSet())) = (dom (.: (F _V))) /\ (G1 .componentSet()) by RELAT_1:61
.= (bool (dom (F _V))) /\ (G1 .componentSet()) by FUNCT_3:def 1
.= G1 .componentSet() by A2, XBOOLE_1:28 ;
thus G1 .numComponents() = card (G1 .componentSet()) by GLIB_002:def 9
.= card { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } by A3, A4, A5, CARD_1:70
.= card (G2 .componentSet()) by A1, Th83
.= G2 .numComponents() by GLIB_002:def 9 ; :: thesis: verum