let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
G2 .componentSet() = { ((F _V) .: C) where C is Element of G1 .componentSet() : verum }
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies G2 .componentSet() = { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } )
set S = { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } ;
assume A1: F is isomorphism ; :: thesis: G2 .componentSet() = { ((F _V) .: C) where C is Element of G1 .componentSet() : verum }

now :: thesis: for x being object holds
( ( x in G2 .componentSet() implies x in { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } ) & ( x in { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } implies x in G2 .componentSet() ) )

let x be object ; :: thesis: ( ( x in G2 .componentSet() implies x in { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } ) & ( x in { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } implies x in G2 .componentSet() ) )
reconsider X = x as set by TARSKI:1;

hereby :: thesis: ( x in { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } implies x in G2 .componentSet() )

assume x in G2 .componentSet() ; :: thesis: x in { ((F _V) .: C) where C is Element of G1 .componentSet() : verum }
then consider v2 being Vertex of G2 such that
A2: X = G2 .reachableFrom v2 by GLIB_002:def 8;
the_Vertices_of G2 = rng (F _V) by A1, GLIB_010:def 12;
then consider v1 being object such that
A3: ( v1 in dom (F _V) & (F _V) . v1 = v2 ) by FUNCT_1:def 3;
reconsider v1 = v1 as Vertex of G1 by A3;
A4: X = (F _V) .: (G1 .reachableFrom v1) by A1, A2, A3, Th82;
G1 .reachableFrom v1 in G1 .componentSet() by GLIB_002:def 8;
hence x in { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } by A4; :: thesis: verum

end;

assume x in { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } ; :: thesis: x in G2 .componentSet()
then consider C being Element of G1 .componentSet() such that
A5: x = (F _V) .: C ;
consider v1 being Vertex of G1 such that
A6: C = G1 .reachableFrom v1 by GLIB_002:def 8;
the_Vertices_of G1 = dom (F _V) by A1, GLIB_010:def 11;
then (F _V) . v1 in rng (F _V) by FUNCT_1:3;
then reconsider v2 = (F _V) . v1 as Vertex of G2 ;
x = G2 .reachableFrom v2 by A1, A5, A6, Th82;
hence x in G2 .componentSet() by GLIB_002:def 8; :: thesis: verum

end;

hence G2 .componentSet() = { ((F _V) .: C) where C is Element of G1 .componentSet() : verum } by TARSKI:2; :: thesis: verum