let G1, G2 be _Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( (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()) ; :: thesis: W1 .first() = W1 .last()
per cases ( len W1 >= 3 or not len W1 >= 3 ) ;
suppose A3: len W1 >= 3 ; :: thesis: 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; :: thesis: verum
end;
suppose not len W1 >= 3 ; :: thesis: W1 .first() = W1 .last()
hence W1 .first() = W1 .last() by GLIB_001:125, GLIB_001:127; :: thesis: verum
end;
end;