let G1, G2 be _Graph; for F being PGraphMapping of G1,G2 st F is one-to-one & F is onto holds
G2 .allConnectedSG() c= rng ((SG2SGFunc F) | (G1 .allConnectedSG()))
let F be PGraphMapping of G1,G2; ( F is one-to-one & F is onto implies G2 .allConnectedSG() c= rng ((SG2SGFunc F) | (G1 .allConnectedSG())) )
assume A1:
( F is one-to-one & F is onto )
; G2 .allConnectedSG() c= rng ((SG2SGFunc F) | (G1 .allConnectedSG()))
set f = (SG2SGFunc F) | (G1 .allConnectedSG());
A2:
dom ((SG2SGFunc F) | (G1 .allConnectedSG())) = G1 .allConnectedSG()
by FUNCT_2:def 1;
now for x being object st x in G2 .allConnectedSG() holds
x in rng ((SG2SGFunc F) | (G1 .allConnectedSG()))let x be
object ;
( x in G2 .allConnectedSG() implies x in rng ((SG2SGFunc F) | (G1 .allConnectedSG())) )assume
x in G2 .allConnectedSG()
;
x in rng ((SG2SGFunc F) | (G1 .allConnectedSG()))then reconsider H2 =
x as
connected plain Subgraph of
G2 by Th124;
rng F == G2
by A1, GLIB_010:56;
then A3:
H2 is
Subgraph of
rng F
by GLIB_000:91;
set H1 = the
plain inducedSubgraph of
G1,
(F _V) " (the_Vertices_of H2),
(F _E) " (the_Edges_of H2);
the
plain inducedSubgraph of
G1,
(F _V) " (the_Vertices_of H2),
(F _E) " (the_Edges_of H2) is
connected
by A1, A3, GLIBPRE1:108;
then A4:
the
plain inducedSubgraph of
G1,
(F _V) " (the_Vertices_of H2),
(F _E) " (the_Edges_of H2) in dom ((SG2SGFunc F) | (G1 .allConnectedSG()))
by A2, Th124;
A5:
rng (F | the plain inducedSubgraph of G1,(F _V) " (the_Vertices_of H2),(F _E) " (the_Edges_of H2)) = H2
by A1, A3, GLIB_009:44, GLIBPRE1:99;
((SG2SGFunc F) | (G1 .allConnectedSG())) . the
plain inducedSubgraph of
G1,
(F _V) " (the_Vertices_of H2),
(F _E) " (the_Edges_of H2) =
(SG2SGFunc F) . the
plain inducedSubgraph of
G1,
(F _V) " (the_Vertices_of H2),
(F _E) " (the_Edges_of H2)
by A4, FUNCT_1:47
.=
H2
by A5, Def5
;
hence
x in rng ((SG2SGFunc F) | (G1 .allConnectedSG()))
by A4, FUNCT_1:3;
verum end;
hence
G2 .allConnectedSG() c= rng ((SG2SGFunc F) | (G1 .allConnectedSG()))
by TARSKI:def 3; verum