let G1, G2 be _Graph; for F being non empty one-to-one PGraphMapping of G1,G2 st F is isomorphism holds
G2 .allComponents() = rng ((SG2SGFunc F) | (G1 .allComponents()))
let F be non empty one-to-one PGraphMapping of G1,G2; ( F is isomorphism implies G2 .allComponents() = rng ((SG2SGFunc F) | (G1 .allComponents())) )
set f = SG2SGFunc F;
A1:
dom ((SG2SGFunc F) | (G1 .allComponents())) = G1 .allComponents()
by FUNCT_2:def 1;
assume A2:
F is isomorphism
; G2 .allComponents() = rng ((SG2SGFunc F) | (G1 .allComponents()))
now for y being object holds
( ( y in G2 .allComponents() implies y in rng ((SG2SGFunc F) | (G1 .allComponents())) ) & ( y in rng ((SG2SGFunc F) | (G1 .allComponents())) implies y in G2 .allComponents() ) )let y be
object ;
( ( y in G2 .allComponents() implies y in rng ((SG2SGFunc F) | (G1 .allComponents())) ) & ( y in rng ((SG2SGFunc F) | (G1 .allComponents())) implies y in G2 .allComponents() ) )hereby ( y in rng ((SG2SGFunc F) | (G1 .allComponents())) implies y in G2 .allComponents() )
assume
y in G2 .allComponents()
;
y in rng ((SG2SGFunc F) | (G1 .allComponents()))then reconsider C2 =
y as
plain Component of
G2 by Th189;
set v2 = the
Vertex of
C2;
the_Vertices_of C2 c= the_Vertices_of G2
;
then reconsider v2 = the
Vertex of
C2 as
Vertex of
G2 by TARSKI:def 3;
A3:
the_Vertices_of C2 = G2 .reachableFrom v2
by GLIB_002:33;
the_Edges_of C2 = G2 .edgesBetween (the_Vertices_of C2)
by GLIB_002:31;
then A4:
C2 is
inducedSubgraph of
G2,
(G2 .reachableFrom v2)
by A3, GLIB_000:170;
A5:
G2 == rng F
by A2, GLIB_010:56;
then
G2 .edgesBetween (G2 .reachableFrom v2) = (rng F) .edgesBetween (G2 .reachableFrom v2)
by GLIB_000:90;
then reconsider C2 =
C2 as
inducedSubgraph of
(rng F),
(G2 .reachableFrom v2) by A4, A5, GLIB_000:95;
set C1 = the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of C2));
A6:
dom (F _E) = the_Edges_of G1
by A2, GLIB_010:def 11;
the_Vertices_of G2 = the_Vertices_of (rng F)
by A5, GLIB_000:def 34;
then A7:
C2 =
rng (F | the plain inducedSubgraph of G1,((F _V) " (the_Vertices_of C2)))
by A6, GLIB_009:44, GLIBPRE1:101
.=
(SG2SGFunc F) . the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of C2))
by Def5
;
rng (F _V) = the_Vertices_of G2
by A2, GLIB_010:def 12;
then consider v1 being
object such that A8:
(
v1 in dom (F _V) &
(F _V) . v1 = v2 )
by FUNCT_1:def 3;
reconsider v1 =
v1 as
Vertex of
G1 by A8;
(F _V) " (the_Vertices_of C2) = G1 .reachableFrom v1
by A2, A3, A8, GLIBPRE1:97;
then
( the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of C2)) in dom ((SG2SGFunc F) | (G1 .allComponents())) &
C2 = ((SG2SGFunc F) | (G1 .allComponents())) . the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of C2)) )
by A1, A7, Th189, FUNCT_1:49;
hence
y in rng ((SG2SGFunc F) | (G1 .allComponents()))
by FUNCT_1:def 3;
verum
end; assume
y in rng ((SG2SGFunc F) | (G1 .allComponents()))
;
y in G2 .allComponents() then consider x being
object such that A9:
(
x in dom ((SG2SGFunc F) | (G1 .allComponents())) &
((SG2SGFunc F) | (G1 .allComponents())) . x = y )
by FUNCT_1:def 3;
reconsider C1 =
x as
Component-like plain Subgraph of
G1 by A9, Th189;
set v1 = the
Vertex of
C1;
the_Vertices_of C1 c= the_Vertices_of G1
;
then reconsider v1 = the
Vertex of
C1 as
Vertex of
G1 by TARSKI:def 3;
A10:
y =
(SG2SGFunc F) . C1
by A9, FUNCT_1:47
.=
rng (F | C1)
by Def5
;
dom (F _V) = the_Vertices_of G1
by A2, 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 ;
A11:
(F _V) .: (the_Vertices_of C1) =
(F _V) .: (G1 .reachableFrom v1)
by GLIB_002:33
.=
G2 .reachableFrom v2
by A2, GLIBPRE1:81
;
A12:
rng ((F | C1) _V) = G2 .reachableFrom v2
by A11, RELAT_1:115;
rng ((F | C1) _E) =
(F _E) .: (the_Edges_of C1)
by RELAT_1:115
.=
(F _E) .: (G1 .edgesBetween (the_Vertices_of C1))
by GLIB_002:31
.=
G2 .edgesBetween (G2 .reachableFrom v2)
by A2, A11, GLIBPRE1:93
;
hence
y in G2 .allComponents()
by A10, A12, Th189;
verum end;
hence
G2 .allComponents() = rng ((SG2SGFunc F) | (G1 .allComponents()))
by TARSKI:2; verum