let G1, G2 be _Graph; for F being PGraphMapping of G1,G2 st F is total & F is onto holds
G2 .allInducedSG() c= rng ((SG2SGFunc F) | (G1 .allInducedSG()))
let F be PGraphMapping of G1,G2; ( F is total & F is onto implies G2 .allInducedSG() c= rng ((SG2SGFunc F) | (G1 .allInducedSG())) )
assume A1:
( F is total & F is onto )
; G2 .allInducedSG() c= rng ((SG2SGFunc F) | (G1 .allInducedSG()))
set f = (SG2SGFunc F) | (G1 .allInducedSG());
A2:
dom ((SG2SGFunc F) | (G1 .allInducedSG())) = G1 .allInducedSG()
by FUNCT_2:def 1;
now for x being object st x in G2 .allInducedSG() holds
x in rng ((SG2SGFunc F) | (G1 .allInducedSG()))let x be
object ;
( x in G2 .allInducedSG() implies x in rng ((SG2SGFunc F) | (G1 .allInducedSG())) )assume A3:
x in G2 .allInducedSG()
;
x in rng ((SG2SGFunc F) | (G1 .allInducedSG()))A4:
rng F == G2
by A1, GLIB_010:56;
then
x in (rng F) .allInducedSG()
by A3, Th49;
then consider V2 being non
empty Subset of
(the_Vertices_of (rng F)) such that A5:
x = the
plain inducedSubgraph of
(rng F),
V2
;
reconsider H2 =
x as
plain inducedSubgraph of
(rng F),
V2 by A5;
set H1 = the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of H2));
reconsider y = the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of H2)) as
object ;
rng (F _V) =
the_Vertices_of G2
by A1, GLIB_010:def 12
.=
the_Vertices_of (rng F)
by A4, GLIB_000:def 34
;
then A6:
(F _V) " V2 <> {}
by RELAT_1:139;
the_Vertices_of H2 = V2
by GLIB_000:def 37;
then A7:
the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of H2)) in G1 .allInducedSG()
by A6;
then A8:
y in dom ((SG2SGFunc F) | (G1 .allInducedSG()))
by A2;
A9:
(SG2SGFunc F) . the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of H2)) = rng (F | the plain inducedSubgraph of G1,((F _V) " (the_Vertices_of H2)))
by Def5;
dom (F _E) = the_Edges_of G1
by A1, GLIB_010:def 11;
then
G1 .edgesBetween ((F _V) " (the_Vertices_of H2)) c= dom (F _E)
;
then
(SG2SGFunc F) . the
plain inducedSubgraph of
G1,
((F _V) " (the_Vertices_of H2)) = H2
by A1, A9, GLIB_009:44, GLIBPRE1:101;
then
x = ((SG2SGFunc F) | (G1 .allInducedSG())) . y
by A7, FUNCT_1:49;
hence
x in rng ((SG2SGFunc F) | (G1 .allInducedSG()))
by A8, FUNCT_1:def 3;
verum end;
hence
G2 .allInducedSG() c= rng ((SG2SGFunc F) | (G1 .allInducedSG()))
by TARSKI:def 3; verum