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 that

A1: m <= n and

A2: n <= len W and

A3: W . m = W . n ; :: thesis: (W .cut (1,m)) .last() = (W .cut (n,(len W))) .first()

A4: 1 <= m by ABIAN:12;

m <= len W by A1, A2, XXREAL_0:2;

hence (W .cut (1,m)) .last() = W . n by A3, A4, Lm16, JORDAN12:2

.= (W .cut (n,(len W))) .first() by A2, Lm16 ;

:: thesis: verum

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 that

A1: m <= n and

A2: n <= len W and

A3: W . m = W . n ; :: thesis: (W .cut (1,m)) .last() = (W .cut (n,(len W))) .first()

A4: 1 <= m by ABIAN:12;

m <= len W by A1, A2, XXREAL_0:2;

hence (W .cut (1,m)) .last() = W . n by A3, A4, Lm16, JORDAN12:2

.= (W .cut (n,(len W))) .first() by A2, Lm16 ;

:: thesis: verum