let G1, G2 be _Graph; for F being PGraphMapping of G1,G2 st F is total holds
rng ((SG2SGFunc F) | (G1 .allConnectedSG())) c= G2 .allConnectedSG()
let F be PGraphMapping of G1,G2; ( F is total implies rng ((SG2SGFunc F) | (G1 .allConnectedSG())) c= G2 .allConnectedSG() )
assume A1:
F is total
; rng ((SG2SGFunc F) | (G1 .allConnectedSG())) c= G2 .allConnectedSG()
set f = (SG2SGFunc F) | (G1 .allConnectedSG());
now for y being object st y in rng ((SG2SGFunc F) | (G1 .allConnectedSG())) holds
y in G2 .allConnectedSG() let y be
object ;
( y in rng ((SG2SGFunc F) | (G1 .allConnectedSG())) implies y in G2 .allConnectedSG() )assume A2:
y in rng ((SG2SGFunc F) | (G1 .allConnectedSG()))
;
y in G2 .allConnectedSG() then consider x being
object such that A3:
(
x in dom ((SG2SGFunc F) | (G1 .allConnectedSG())) &
((SG2SGFunc F) | (G1 .allConnectedSG())) . x = y )
by FUNCT_1:def 3;
reconsider H1 =
x as
connected plain Subgraph of
G1 by A3, Th124;
y in rng (SG2SGFunc F)
by A2, TARSKI:def 3, RELAT_1:70;
then reconsider H2 =
y as
plain Subgraph of
G2 by Th1;
A4:
H2 =
(SG2SGFunc F) . x
by A3, FUNCT_1:47
.=
rng (F | H1)
by Def5
;
now for v2, w2 being Vertex of H2 ex W2 being Walk of H2 st W2 is_Walk_from v2,w2let v2,
w2 be
Vertex of
H2;
ex W2 being Walk of H2 st W2 is_Walk_from v2,w2A5:
F | H1 is
total
by A1, GLIB_010:57;
A6:
the_Vertices_of H2 = rng ((F | H1) _V)
by A4, A5, GLIB_010:54;
then consider v1 being
object such that A7:
(
v1 in dom ((F | H1) _V) &
((F | H1) _V) . v1 = v2 )
by FUNCT_1:def 3;
consider w1 being
object such that A8:
(
w1 in dom ((F | H1) _V) &
((F | H1) _V) . w1 = w2 )
by A6, FUNCT_1:def 3;
reconsider v1 =
v1,
w1 =
w1 as
Vertex of
H1 by A7, A8;
consider W1 being
Walk of
H1 such that A9:
W1 is_Walk_from v1,
w1
by GLIB_002:def 1;
reconsider F9 =
F | H1 as non
empty PGraphMapping of
H1,
rng (F | H1) by A5, GLIBPRE1:88;
F9 is
total
by A1, GLIBPRE1:109;
then reconsider W1 =
W1 as
F9 -defined Walk of
H1 by GLIB_010:121;
reconsider W2 =
F9 .: W1 as
Walk of
H2 by A4;
take W2 =
W2;
W2 is_Walk_from v2,w2
F9 .: W1 is_Walk_from (F9 _V) . v1,
(F9 _V) . w1
by A9, GLIB_010:132;
hence
W2 is_Walk_from v2,
w2
by A7, A8, GLIB_001:19;
verum end; then
H2 is
connected
by GLIB_002:def 1;
hence
y in G2 .allConnectedSG()
by Th124;
verum end;
hence
rng ((SG2SGFunc F) | (G1 .allConnectedSG())) c= G2 .allConnectedSG()
by TARSKI:def 3; verum