let G1, G2 be _Graph; for F being non empty one-to-one PGraphMapping of G1,G2
for W1 being b1 -defined Walk of G1 st (F _V) . (W1 .first()) = (F _V) . (W1 .last()) holds
W1 .first() = W1 .last()
let F be non empty one-to-one PGraphMapping of G1,G2; for W1 being F -defined Walk of G1 st (F _V) . (W1 .first()) = (F _V) . (W1 .last()) holds
W1 .first() = W1 .last()
let W1 be F -defined Walk of G1; ( (F _V) . (W1 .first()) = (F _V) . (W1 .last()) implies W1 .first() = W1 .last() )
A1:
F is semi-continuous
;
assume A2:
(F _V) . (W1 .first()) = (F _V) . (W1 .last())
; W1 .first() = W1 .last()
per cases
( len W1 >= 3 or not len W1 >= 3 )
;
suppose A3:
len W1 >= 3
;
W1 .first() = W1 .last() then
1
< len W1
by XXREAL_0:2;
then A4:
W1 . (1 + 1) Joins W1 . 1,
W1 . (1 + 2),
G1
by POLYFORM:4, GLIB_001:def 3;
A5:
(
W1 . 1
in W1 .vertices() &
W1 . 3
in W1 .vertices() &
W1 .last() in W1 .vertices() )
by A3, XXREAL_0:2, GLIB_001:87, GLIB_001:88, POLYFORM:4, POLYFORM:6;
( 1
<= 2 & 2
<= len W1 )
by A3, XXREAL_0:2;
then
W1 . 2
in W1 .edges()
by POLYFORM:5, GLIB_001:99;
then A6:
(
W1 . 1
in dom (F _V) &
W1 . 2
in dom (F _E) &
W1 . 3
in dom (F _V) &
W1 .last() in dom (F _V) )
by A5, Def35, TARSKI:def 3;
(F _E) . (W1 . 2) Joins (F _V) . (W1 . 1),
(F _V) . (W1 . 3),
G2
by A6, A4, Th4;
then
(F _E) . (W1 . 2) Joins (F _V) . (W1 .last()),
(F _V) . (W1 . 3),
G2
by A2, GLIB_001:def 6;
then
W1 . 2
Joins W1 .last() ,
W1 . 3,
G1
by A1, A6;
then
( (
W1 . 1
= W1 .last() &
W1 . 3
= W1 . 3 ) or (
W1 . 1
= W1 . 3 &
W1 . 3
= W1 .last() ) )
by A4, GLIB_000:15;
hence
W1 .first() = W1 .last()
by GLIB_001:def 6;
verum end;