let G be _Graph; :: thesis: for W being Walk of G st ( for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds

m = n ) holds

W is Path-like

let W be Walk of G; :: thesis: ( ( for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds

m = n ) implies W is Path-like )

assume A1: for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds

m = n ; :: thesis: W is Path-like

m = n ) holds

W is Path-like

let W be Walk of G; :: thesis: ( ( for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds

m = n ) implies W is Path-like )

assume A1: for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds

m = n ; :: thesis: W is Path-like

now :: thesis: for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n

then A21:
W is Trail-like
by Lm57;W . m <> W . n

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

m <= len W by A3, A4, XXREAL_0:2;

then A5: m in dom W by A2, FINSEQ_3:25;

1 <= n by A2, A3, XXREAL_0:2;

then A6: n in dom W by A4, FINSEQ_3:25;

end;assume that

A2: 1 <= m and

A3: m < n and

A4: n <= len W ; :: thesis: W . m <> W . n

m <= len W by A3, A4, XXREAL_0:2;

then A5: m in dom W by A2, FINSEQ_3:25;

1 <= n by A2, A3, XXREAL_0:2;

then A6: n in dom W by A4, FINSEQ_3:25;

now :: thesis: not W . m = W . n

hence
W . m <> W . n
; :: thesis: verumassume
W . m = W . n
; :: thesis: contradiction

then consider naa1 being odd Element of NAT such that

A7: naa1 = n - 1 and

A8: n - 1 in dom W and

A9: n + 1 in dom W and

A10: W . m Joins W . naa1,W . (n + 1),G by A6, Lm2;

A11: naa1 <= len W by A7, A8, FINSEQ_3:25;

consider maa1 being odd Element of NAT such that

A12: maa1 = m - 1 and

A13: m - 1 in dom W and

A14: m + 1 in dom W and

A15: W . m Joins W . maa1,W . (m + 1),G by A5, Lm2;

A16: maa1 <= len W by A12, A13, FINSEQ_3:25;

A17: n + 1 <= len W by A9, FINSEQ_3:25;

A18: m + 1 <= len W by A14, FINSEQ_3:25;

end;then consider naa1 being odd Element of NAT such that

A7: naa1 = n - 1 and

A8: n - 1 in dom W and

A9: n + 1 in dom W and

A10: W . m Joins W . naa1,W . (n + 1),G by A6, Lm2;

A11: naa1 <= len W by A7, A8, FINSEQ_3:25;

consider maa1 being odd Element of NAT such that

A12: maa1 = m - 1 and

A13: m - 1 in dom W and

A14: m + 1 in dom W and

A15: W . m Joins W . maa1,W . (m + 1),G by A5, Lm2;

A16: maa1 <= len W by A12, A13, FINSEQ_3:25;

A17: n + 1 <= len W by A9, FINSEQ_3:25;

A18: m + 1 <= len W by A14, FINSEQ_3:25;

now :: thesis: contradiction

hence
contradiction
; :: thesis: verumend;

now :: thesis: for m, n being odd Element of NAT st m < n & n <= len W & W . m = W . n holds

( m = 1 & n = len W )

hence
W is Path-like
by A21; :: thesis: verum( m = 1 & n = len W )

let m, n be odd Element of NAT ; :: thesis: ( m < n & n <= len W & W . m = W . n implies ( m = 1 & n = len W ) )

assume that

A22: m < n and

A23: n <= len W ; :: thesis: ( W . m = W . n implies ( m = 1 & n = len W ) )

assume A24: W . m = W . n ; :: thesis: ( m = 1 & n = len W )

m <= len W by A22, A23, XXREAL_0:2;

hence ( m = 1 & n = len W ) by A1, A22, A23, A24; :: thesis: verum

end;assume that

A22: m < n and

A23: n <= len W ; :: thesis: ( W . m = W . n implies ( m = 1 & n = len W ) )

assume A24: W . m = W . n ; :: thesis: ( m = 1 & n = len W )

m <= len W by A22, A23, XXREAL_0:2;

hence ( m = 1 & n = len W ) by A1, A22, A23, A24; :: thesis: verum