let G be _Graph; :: thesis: for W being Walk of G holds
( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n )

let W be Walk of G; :: thesis: ( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n )

hereby :: thesis: ( ( for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n ) implies W is Trail-like )
assume W is Trail-like ; :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n

then A1: W .edgeSeq() is one-to-one ;
let m, n be even Element of NAT ; :: thesis: ( 1 <= m & m < n & n <= len W implies W . m <> W . n )
assume that
A2: 1 <= m and
A3: m < n and
A4: n <= len W ; :: thesis: W . m <> W . n
A5: 1 <= n by ;
then A6: n div 2 in dom () by ;
A7: m <= len W by ;
then A8: W . m = () . (m div 2) by ;
A9: now :: thesis: not m div 2 = n div 2end;
A12: W . n = () . (n div 2) by A4, A5, Lm40;
m div 2 in dom () by A2, A7, Lm40;
hence W . m <> W . n by ; :: thesis: verum
end;
assume A13: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds
W . m <> W . n ; :: thesis: W is Trail-like
now :: thesis: for x1, x2 being object st x1 in dom () & x2 in dom () & () . x1 = () . x2 holds
x1 = x2
let x1, x2 be object ; :: thesis: ( x1 in dom () & x2 in dom () & () . x1 = () . x2 implies x1 = x2 )
assume that
A14: x1 in dom () and
A15: x2 in dom () and
A16: (W .edgeSeq()) . x1 = () . x2 ; :: thesis: x1 = x2
reconsider m = x1, n = x2 as Element of NAT by ;
A17: m <= len () by ;
1 <= m by ;
then A18: (W .edgeSeq()) . x1 = W . (2 * m) by ;
A19: n <= len () by ;
1 <= n by ;
then A20: W . (2 * m) = W . (2 * n) by ;
A21: 2 * n in dom W by ;
then A22: 1 <= 2 * n by FINSEQ_3:25;
A23: 2 * m in dom W by ;
then A24: 2 * m <= len W by FINSEQ_3:25;
A25: 2 * n <= len W by ;
A26: 1 <= 2 * m by ;
now :: thesis: x1 = x2
per cases ( 2 * m < 2 * n or 2 * m = 2 * n or 2 * m > 2 * n ) by XXREAL_0:1;
suppose 2 * m < 2 * n ; :: thesis: x1 = x2
hence x1 = x2 by A13, A20, A26, A25; :: thesis: verum
end;
suppose 2 * m = 2 * n ; :: thesis: x1 = x2
hence x1 = x2 ; :: thesis: verum
end;
suppose 2 * m > 2 * n ; :: thesis: x1 = x2
hence x1 = x2 by A13, A20, A24, A22; :: thesis: verum
end;
end;
end;
hence x1 = x2 ; :: thesis: verum
end;
then W .edgeSeq() is one-to-one by FUNCT_1:def 4;
hence W is Trail-like ; :: thesis: verum