let G1, G2 be non-multi _Graph; for f being PVertexMapping of G1,G2 st f is total & f is one-to-one & f is continuous holds
for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
let f be PVertexMapping of G1,G2; ( f is total & f is one-to-one & f is continuous implies for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)})) )
assume A1:
( f is total & f is one-to-one & f is continuous )
; for v, w being Vertex of G1 holds card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
let v, w be Vertex of G1; card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
per cases
( G1 .edgesBetween ({v},{w}) = {} or G1 .edgesBetween ({v},{w}) <> {} )
;
suppose A2:
G1 .edgesBetween (
{v},
{w})
= {}
;
card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
G2 .edgesBetween (
{(f . v)},
{(f . w)})
= {}
proof
assume
G2 .edgesBetween (
{(f . v)},
{(f . w)})
<> {}
;
contradiction
then consider e2 being
object such that A3:
G2 .edgesBetween (
{(f . v)},
{(f . w)})
= {e2}
by ZFMISC_1:131;
set v1 =
(the_Source_of G2) . e2;
set v2 =
(the_Target_of G2) . e2;
e2 in G2 .edgesBetween (
{(f . v)},
{(f . w)})
by A3, TARSKI:def 1;
then
e2 SJoins {(f . v)},
{(f . w)},
G2
by GLIB_000:def 30;
then A4:
(
e2 in the_Edges_of G2 & ( (
(the_Source_of G2) . e2 in {(f . v)} &
(the_Target_of G2) . e2 in {(f . w)} ) or (
(the_Source_of G2) . e2 in {(f . w)} &
(the_Target_of G2) . e2 in {(f . v)} ) ) )
by GLIB_000:def 15;
then
( (
(the_Source_of G2) . e2 = f . v &
(the_Target_of G2) . e2 = f . w ) or (
(the_Source_of G2) . e2 = f . w &
(the_Target_of G2) . e2 = f . v ) )
by TARSKI:def 1;
then A5:
e2 Joins f . v,
f . w,
G2
by A4, GLIB_000:def 13;
(
v in the_Vertices_of G1 &
w in the_Vertices_of G1 &
f is
total )
by A1;
then
(
v in dom f &
w in dom f )
by FUNCT_2:def 1;
then consider e1 being
object such that A6:
e1 Joins v,
w,
G1
by A1, A5, Th2;
(
v in {v} &
w in {w} )
by TARSKI:def 1;
then
e1 SJoins {v},
{w},
G1
by A6, GLIB_000:17;
hence
contradiction
by A2, GLIB_000:def 30;
verum
end; hence
card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
by A2;
verum end; suppose
G1 .edgesBetween (
{v},
{w})
<> {}
;
card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))then consider e1 being
object such that A7:
G1 .edgesBetween (
{v},
{w})
= {e1}
by ZFMISC_1:131;
set v1 =
(the_Source_of G1) . e1;
set v2 =
(the_Target_of G1) . e1;
e1 in G1 .edgesBetween (
{v},
{w})
by A7, TARSKI:def 1;
then
e1 SJoins {v},
{w},
G1
by GLIB_000:def 30;
then A8:
(
e1 in the_Edges_of G1 & ( (
(the_Source_of G1) . e1 in {v} &
(the_Target_of G1) . e1 in {w} ) or (
(the_Source_of G1) . e1 in {w} &
(the_Target_of G1) . e1 in {v} ) ) )
by GLIB_000:def 15;
then
( (
(the_Source_of G1) . e1 = v &
(the_Target_of G1) . e1 = w ) or (
(the_Source_of G1) . e1 = w &
(the_Target_of G1) . e1 = v ) )
by TARSKI:def 1;
then A9:
e1 Joins v,
w,
G1
by A8, GLIB_000:def 13;
(
v in the_Vertices_of G1 &
w in the_Vertices_of G1 &
f is
total )
by A1;
then
(
v in dom f &
w in dom f )
by FUNCT_2:def 1;
then consider e2 being
object such that A10:
e2 Joins f . v,
f . w,
G2
by A9, Th1;
(
f . v in {(f . v)} &
f . w in {(f . w)} )
by TARSKI:def 1;
then
e2 SJoins {(f . v)},
{(f . w)},
G2
by A10, GLIB_000:17;
then
e2 in G2 .edgesBetween (
{(f . v)},
{(f . w)})
by GLIB_000:def 30;
then consider e being
object such that A11:
G2 .edgesBetween (
{(f . v)},
{(f . w)})
= {e}
by ZFMISC_1:131;
(
card (G1 .edgesBetween ({v},{w})) = 1 &
card (G2 .edgesBetween ({(f . v)},{(f . w)})) = 1 )
by A7, A11, CARD_1:30;
hence
card (G1 .edgesBetween ({v},{w})) = card (G2 .edgesBetween ({(f . v)},{(f . w)}))
;
verum end; end;