let G1, G2 be _Graph; :: thesis: 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; :: thesis: card ((dom F) .loops()) c= card ((rng F) .loops())

let F be non empty one-to-one PGraphMapping of G1,G2; :: thesis: card ((dom F) .loops()) c= card ((rng F) .loops())

now :: thesis: ex f being Function st

( f is one-to-one & dom f = (dom F) .loops() & rng f c= (rng F) .loops() )

hence
card ((dom F) .loops()) c= card ((rng F) .loops())
by CARD_1:10; :: thesis: verum( 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; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: rng f c= (rng F) .loops()

end;take f = f; :: thesis: ( 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; :: thesis: ( 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 ; :: thesis: rng f c= (rng F) .loops()

now :: thesis: for y being object st y in rng f holds

y in (rng F) .loops()

hence
rng f c= (rng F) .loops()
by TARSKI:def 3; :: thesis: verumy in (rng F) .loops()

let y be object ; :: thesis: ( y in rng f implies y in (rng F) .loops() )

assume y in rng f ; :: thesis: 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; :: thesis: verum

end;assume y in rng f ; :: thesis: 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; :: thesis: verum