let G be _Graph; :: thesis: for W being Walk of G ex lenWaa1 being even Element of NAT st

( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )

let W be Walk of G; :: thesis: ex lenWaa1 being even Element of NAT st

( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )

set lenWaa1 = (len W) - 1;

reconsider lenWaa1 = (len W) - 1 as even Element of NAT by ABIAN:12, INT_1:5;

take lenWaa1 ; :: thesis: ( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )

thus lenWaa1 = (len W) - 1 ; :: thesis: len (W .edgeSeq()) = lenWaa1 div 2

2 divides lenWaa1 by PEPIN:22;

then A1: lenWaa1 = 2 * (lenWaa1 div 2) by NAT_D:3;

len W = (2 * (len (W .edgeSeq()))) + 1 by Def15;

hence len (W .edgeSeq()) = lenWaa1 div 2 by A1; :: thesis: verum

( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )

let W be Walk of G; :: thesis: ex lenWaa1 being even Element of NAT st

( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )

set lenWaa1 = (len W) - 1;

reconsider lenWaa1 = (len W) - 1 as even Element of NAT by ABIAN:12, INT_1:5;

take lenWaa1 ; :: thesis: ( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )

thus lenWaa1 = (len W) - 1 ; :: thesis: len (W .edgeSeq()) = lenWaa1 div 2

2 divides lenWaa1 by PEPIN:22;

then A1: lenWaa1 = 2 * (lenWaa1 div 2) by NAT_D:3;

len W = (2 * (len (W .edgeSeq()))) + 1 by Def15;

hence len (W .edgeSeq()) = lenWaa1 div 2 by A1; :: thesis: verum