let G be _Graph; :: thesis: for W being Walk of G
for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
(W .cut 1,m) .last() = (W .cut n,(len W)) .first()
let W be Walk of G; :: thesis: for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds
(W .cut 1,m) .last() = (W .cut n,(len W)) .first()
let m, n be odd Element of NAT ; :: thesis: ( m <= n & n <= len W & W . m = W . n implies (W .cut 1,m) .last() = (W .cut n,(len W)) .first() )
assume A1: ( m <= n & n <= len W & W . m = W . n ) ; :: thesis: (W .cut 1,m) .last() = (W .cut n,(len W)) .first()
then A2: m <= len W by XXREAL_0:2;
( 1 <= m & not 1 is even ) by HEYTING3:1, JORDAN12:3;
hence (W .cut 1,m) .last() = W . n by A1, A2, Lm16
.= (W .cut n,(len W)) .first() by A1, Lm16 ;
:: thesis: verum