let G1, G2 be _Graph; for F being non empty one-to-one PGraphMapping of G1,G2 holds card ((dom F) .loops()) c= card ((rng F) .loops())
let F be non empty one-to-one PGraphMapping of G1,G2; card ((dom F) .loops()) c= card ((rng F) .loops())
now ex f being Function st
( f is one-to-one & dom f = (dom F) .loops() & rng f c= (rng F) .loops() )reconsider f =
(F _E) | ((dom F) .loops()) as
Function ;
take f =
f;
( f is one-to-one & dom f = (dom F) .loops() & rng f c= (rng F) .loops() )thus
f is
one-to-one
by FUNCT_1:52;
( dom f = (dom F) .loops() & rng f c= (rng F) .loops() )
(dom F) .loops() c= the_Edges_of (dom F)
;
then A1:
(dom F) .loops() c= dom (F _E)
by Th54;
thus A2:
dom f =
(dom (F _E)) /\ ((dom F) .loops())
by RELAT_1:61
.=
(dom F) .loops()
by A1, XBOOLE_1:28
;
rng f c= (rng F) .loops() now for y being object st y in rng f holds
y in (rng F) .loops() let y be
object ;
( y in rng f implies y in (rng F) .loops() )assume
y in rng f
;
y in (rng F) .loops() then consider x being
object such that A3:
(
x in dom f &
f . x = y )
by FUNCT_1:def 3;
consider v being
object such that A4:
x Joins v,
v,
dom F
by A2, A3, GLIB_009:def 2;
v in the_Vertices_of (dom F)
by A4, GLIB_000:13;
then A5:
v in dom (F _V)
by Th54;
A6:
x in dom (F _E)
by A3, RELAT_1:57;
(
x is
set &
v is
set )
by TARSKI:1;
then
x Joins v,
v,
G1
by A4, GLIB_000:72;
then A7:
(F _E) . x Joins (F _V) . v,
(F _V) . v,
G2
by A5, A6, Th4;
(F _E) . x in rng (F _E)
by A6, FUNCT_1:3;
then
(F _E) . x in the_Edges_of (rng F)
by Th54;
then
(F _E) . x Joins (F _V) . v,
(F _V) . v,
rng F
by A7, GLIB_000:73;
then
(F _E) . x in (rng F) .loops()
by GLIB_009:def 2;
hence
y in (rng F) .loops()
by A3, FUNCT_1:47;
verum end; hence
rng f c= (rng F) .loops()
by TARSKI:def 3;
verum end;
hence
card ((dom F) .loops()) c= card ((rng F) .loops())
by CARD_1:10; verum