set n = (len W) + 1;

defpred S_{1}[ Nat, set , set ] means ( ( W is Walk of G & ex Wn being Walk of G st

( Wn = W & c_{3} = Wn .remove ((Wn .find ((2 * G) + 1)),(Wn .rfind ((2 * G) + 1))) ) ) or ( W is not Walk of G & c_{3} = W ) );

A2: ( dom f = NAT & f . 0 = W & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 1(A1);

defpred S_{2}[ Nat] means ex Wn being Subwalk of W st

( Wn = f . G & len Wn <= len W & ( for m being odd Element of NAT st m < (2 * G) + 1 & m <= len Wn holds

Wn .rfind m = m ) );

_{2}[n] holds

S_{2}[n + 1]
;

reconsider W0 = f . 0 as Subwalk of W by A2, Lm70;

for m being odd Element of NAT st m < (2 * 0) + 1 & m <= len W0 holds

W0 .rfind m = m by ABIAN:12;

then A58: S_{2}[ 0 ]
by A2;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A58, A57);

then consider P being Subwalk of W such that

P = f . ((len W) + 1) and

A59: len P <= len W and

A60: for m being odd Element of NAT st m < (2 * ((len W) + 1)) + 1 & m <= len P holds

P .rfind m = m ;

take P ; :: thesis: ( P is Trail-like & P is Path-like )

hence ( P is Trail-like & P is Path-like ) ; :: thesis: verum

defpred S

( Wn = W & c

A1: now :: thesis: for n being Nat

for x being set ex y being set st S_{1}[n,x,y]

consider f being Function such that for x being set ex y being set st S

let n be Nat; :: thesis: for x being set ex y being set st S_{1}[n,x,y]

let x be set ; :: thesis: ex y being set st S_{1}[n,x,y]

_{1}[n,x,y]
; :: thesis: verum

end;let x be set ; :: thesis: ex y being set st S

now :: thesis: ex y being set st S_{1}[n,x,y]end;

hence
ex y being set st Sper cases
( x is Walk of G or not x is Walk of G )
;

end;

suppose
x is Walk of G
; :: thesis: ex y being set st S_{1}[n,x,y]

then reconsider W = x as Walk of G ;

set y = W .remove ((W .find ((2 * n) + 1)),(W .rfind ((2 * n) + 1)));

S_{1}[n,x,W .remove ((W .find ((2 * n) + 1)),(W .rfind ((2 * n) + 1)))]
;

hence ex y being set st S_{1}[n,x,y]
; :: thesis: verum

end;set y = W .remove ((W .find ((2 * n) + 1)),(W .rfind ((2 * n) + 1)));

S

hence ex y being set st S

A2: ( dom f = NAT & f . 0 = W & ( for n being Nat holds S

defpred S

( Wn = f . G & len Wn <= len W & ( for m being odd Element of NAT st m < (2 * G) + 1 & m <= len Wn holds

Wn .rfind m = m ) );

now :: thesis: for n being Nat st S_{2}[n] holds

ex Wn1 being Subwalk of W st

( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) )

then A57:
for n being Nat st Sex Wn1 being Subwalk of W st

( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) )

let n be Nat; :: thesis: ( S_{2}[n] implies ex Wn1 being Subwalk of W st

( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) ) )

assume S_{2}[n]
; :: thesis: ex Wn1 being Subwalk of W st

( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) )

then consider Wn being Subwalk of W such that

A3: Wn = f . n and

A4: len Wn <= len W and

A5: for m being odd Element of NAT st m < (2 * n) + 1 & m <= len Wn holds

Wn .rfind m = m ;

set a = Wn .find ((2 * n) + 1);

set b = Wn .rfind ((2 * n) + 1);

set Wn1 = Wn .remove ((Wn .find ((2 * n) + 1)),(Wn .rfind ((2 * n) + 1)));

reconsider Wn1 = Wn .remove ((Wn .find ((2 * n) + 1)),(Wn .rfind ((2 * n) + 1))) as Subwalk of W by Lm71;

take Wn1 = Wn1; :: thesis: ( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) )

S_{1}[n,f . n,f . (n + 1)]
by A2;

hence f . (n + 1) = Wn1 by A3; :: thesis: ( len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) )

len Wn1 <= len Wn by Lm26;

hence len Wn1 <= len W by A4, XXREAL_0:2; :: thesis: for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m

let m be odd Element of NAT ; :: thesis: ( m < (2 * (n + 1)) + 1 & m <= len Wn1 implies Wn1 .rfind m = m )

assume that

A6: m < (2 * (n + 1)) + 1 and

A7: m <= len Wn1 ; :: thesis: Wn1 .rfind m = m

set W1 = Wn .cut (1,(Wn .find ((2 * n) + 1)));

set W2 = Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn));

A8: len Wn1 <= len Wn by Lm26;

then A9: m <= len Wn by A7, XXREAL_0:2;

m <= 2 * (n + 1) by A6, NAT_1:13;

then m < ((2 * n) + 1) + 1 by XXREAL_0:1;

then A10: m <= (2 * n) + 1 by NAT_1:13;

end;( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) ) )

assume S

( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) )

then consider Wn being Subwalk of W such that

A3: Wn = f . n and

A4: len Wn <= len W and

A5: for m being odd Element of NAT st m < (2 * n) + 1 & m <= len Wn holds

Wn .rfind m = m ;

set a = Wn .find ((2 * n) + 1);

set b = Wn .rfind ((2 * n) + 1);

set Wn1 = Wn .remove ((Wn .find ((2 * n) + 1)),(Wn .rfind ((2 * n) + 1)));

reconsider Wn1 = Wn .remove ((Wn .find ((2 * n) + 1)),(Wn .rfind ((2 * n) + 1))) as Subwalk of W by Lm71;

take Wn1 = Wn1; :: thesis: ( f . (n + 1) = Wn1 & len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) )

S

hence f . (n + 1) = Wn1 by A3; :: thesis: ( len Wn1 <= len W & ( for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m ) )

len Wn1 <= len Wn by Lm26;

hence len Wn1 <= len W by A4, XXREAL_0:2; :: thesis: for m being odd Element of NAT st m < (2 * (n + 1)) + 1 & m <= len Wn1 holds

Wn1 .rfind m = m

let m be odd Element of NAT ; :: thesis: ( m < (2 * (n + 1)) + 1 & m <= len Wn1 implies Wn1 .rfind m = m )

assume that

A6: m < (2 * (n + 1)) + 1 and

A7: m <= len Wn1 ; :: thesis: Wn1 .rfind m = m

set W1 = Wn .cut (1,(Wn .find ((2 * n) + 1)));

set W2 = Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn));

A8: len Wn1 <= len Wn by Lm26;

then A9: m <= len Wn by A7, XXREAL_0:2;

m <= 2 * (n + 1) by A6, NAT_1:13;

then m < ((2 * n) + 1) + 1 by XXREAL_0:1;

then A10: m <= (2 * n) + 1 by NAT_1:13;

now :: thesis: Wn1 .rfind m = mend;

hence
Wn1 .rfind m = m
; :: thesis: verumper cases
( (2 * n) + 1 <= len Wn or len Wn < (2 * n) + 1 )
;

end;

suppose A11:
(2 * n) + 1 <= len Wn
; :: thesis: Wn1 .rfind m = m

then A12:
Wn .find ((2 * n) + 1) <= (2 * n) + 1
by Lm49;

A13: Wn . (Wn .find ((2 * n) + 1)) = Wn . ((2 * n) + 1) by A11, Def20;

A14: Wn .find ((2 * n) + 1) <= len Wn by A11, Def20;

A18: Wn . (Wn .rfind ((2 * n) + 1)) = Wn . ((2 * n) + 1) by A11, Def22;

set m9 = Wn1 .rfind m;

A19: 1 <= m by ABIAN:12;

A20: Wn1 . (Wn1 .rfind m) = Wn1 . m by A7, Def22;

A21: Wn1 .rfind m >= m by A7, Lm50;

A22: Wn .rfind ((2 * n) + 1) <= len Wn by A11, Def22;

1 <= Wn .find ((2 * n) + 1) by ABIAN:12;

then A23: (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .last() = Wn . ((2 * n) + 1) by A14, A13, Lm16, JORDAN12:2

.= (Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn))) .first() by A22, A18, Lm16 ;

(2 * n) + 1 <= Wn .rfind ((2 * n) + 1) by A11, Lm50;

then A24: Wn .find ((2 * n) + 1) <= Wn .rfind ((2 * n) + 1) by A12, XXREAL_0:2;

then A25: Wn1 = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .append (Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn))) by A13, A22, A18, Def12;

A26: Wn1 .rfind m <= len Wn1 by A7, Def22;

then A27: Wn1 .rfind m <= len Wn by A8, XXREAL_0:2;

end;A13: Wn . (Wn .find ((2 * n) + 1)) = Wn . ((2 * n) + 1) by A11, Def20;

A14: Wn .find ((2 * n) + 1) <= len Wn by A11, Def20;

A15: now :: thesis: not Wn .find ((2 * n) + 1) < (2 * n) + 1

then A17:
Wn .find ((2 * n) + 1) = (2 * n) + 1
by A12, XXREAL_0:1;assume A16:
Wn .find ((2 * n) + 1) < (2 * n) + 1
; :: thesis: contradiction

then Wn .find ((2 * n) + 1) <= len Wn by A11, XXREAL_0:2;

then Wn .rfind (Wn .find ((2 * n) + 1)) = Wn .find ((2 * n) + 1) by A5, A16;

hence contradiction by A11, A14, A13, A16, Def22; :: thesis: verum

end;then Wn .find ((2 * n) + 1) <= len Wn by A11, XXREAL_0:2;

then Wn .rfind (Wn .find ((2 * n) + 1)) = Wn .find ((2 * n) + 1) by A5, A16;

hence contradiction by A11, A14, A13, A16, Def22; :: thesis: verum

A18: Wn . (Wn .rfind ((2 * n) + 1)) = Wn . ((2 * n) + 1) by A11, Def22;

set m9 = Wn1 .rfind m;

A19: 1 <= m by ABIAN:12;

A20: Wn1 . (Wn1 .rfind m) = Wn1 . m by A7, Def22;

A21: Wn1 .rfind m >= m by A7, Lm50;

A22: Wn .rfind ((2 * n) + 1) <= len Wn by A11, Def22;

1 <= Wn .find ((2 * n) + 1) by ABIAN:12;

then A23: (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .last() = Wn . ((2 * n) + 1) by A14, A13, Lm16, JORDAN12:2

.= (Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn))) .first() by A22, A18, Lm16 ;

(2 * n) + 1 <= Wn .rfind ((2 * n) + 1) by A11, Lm50;

then A24: Wn .find ((2 * n) + 1) <= Wn .rfind ((2 * n) + 1) by A12, XXREAL_0:2;

then A25: Wn1 = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .append (Wn .cut ((Wn .rfind ((2 * n) + 1)),(len Wn))) by A13, A22, A18, Def12;

A26: Wn1 .rfind m <= len Wn1 by A7, Def22;

then A27: Wn1 .rfind m <= len Wn by A8, XXREAL_0:2;

now :: thesis: Wn1 .rfind m = mend;

hence
Wn1 .rfind m = m
; :: thesis: verumper cases
( m < (2 * n) + 1 or m = (2 * n) + 1 )
by A10, XXREAL_0:1;

end;

suppose A28:
m < (2 * n) + 1
; :: thesis: Wn1 .rfind m = m

then
m < len (Wn .cut (1,(Wn .find ((2 * n) + 1))))
by A11, A17, Lm22;

then A29: Wn1 .cut (1,m) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,m) by A25, A19, A23, Lm21, JORDAN12:2

.= Wn .cut (1,m) by A10, A17, Lm20 ;

reconsider maa1 = m - 1 as Element of NAT by ABIAN:12, INT_1:5;

A30: maa1 + 1 = m ;

A31: maa1 < m - 0 by XREAL_1:15;

then A32: maa1 < len (Wn .cut (1,m)) by A7, A8, Lm22, XXREAL_0:2;

maa1 < len (Wn1 .cut (1,m)) by A7, A31, Lm22;

then Wn1 . m = (Wn .cut (1,m)) . m by A7, A19, A29, A30, Lm15, JORDAN12:2;

then A33: Wn1 . m = Wn . m by A9, A19, A30, A32, Lm15, JORDAN12:2;

A34: Wn .rfind m = m by A5, A9, A28;

end;then A29: Wn1 .cut (1,m) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,m) by A25, A19, A23, Lm21, JORDAN12:2

.= Wn .cut (1,m) by A10, A17, Lm20 ;

reconsider maa1 = m - 1 as Element of NAT by ABIAN:12, INT_1:5;

A30: maa1 + 1 = m ;

A31: maa1 < m - 0 by XREAL_1:15;

then A32: maa1 < len (Wn .cut (1,m)) by A7, A8, Lm22, XXREAL_0:2;

maa1 < len (Wn1 .cut (1,m)) by A7, A31, Lm22;

then Wn1 . m = (Wn .cut (1,m)) . m by A7, A19, A29, A30, Lm15, JORDAN12:2;

then A33: Wn1 . m = Wn . m by A9, A19, A30, A32, Lm15, JORDAN12:2;

A34: Wn .rfind m = m by A5, A9, A28;

now :: thesis: Wn1 .rfind m = mend;

hence
Wn1 .rfind m = m
; :: thesis: verumper cases
( Wn1 .rfind m < Wn .find ((2 * n) + 1) or Wn .find ((2 * n) + 1) <= Wn1 .rfind m )
;

end;

suppose A35:
Wn1 .rfind m < Wn .find ((2 * n) + 1)
; :: thesis: Wn1 .rfind m = m

reconsider m9aa1 = (Wn1 .rfind m) - 1 as Element of NAT by ABIAN:12, INT_1:5;

A36: 1 <= Wn1 .rfind m by ABIAN:12;

A37: m9aa1 < (Wn1 .rfind m) - 0 by XREAL_1:15;

then A38: m9aa1 < len (Wn1 .cut (1,(Wn1 .rfind m))) by A26, Lm22;

A39: m9aa1 < len (Wn .cut (1,(Wn1 .rfind m))) by A8, A26, A37, Lm22, XXREAL_0:2;

Wn1 .rfind m < len (Wn .cut (1,(Wn .find ((2 * n) + 1)))) by A14, A35, Lm22;

then Wn1 .cut (1,(Wn1 .rfind m)) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,(Wn1 .rfind m)) by A25, A23, A36, Lm21, JORDAN12:2

.= Wn .cut (1,(Wn1 .rfind m)) by A35, Lm20 ;

then Wn1 . (Wn1 .rfind m) = (Wn .cut (1,(Wn1 .rfind m))) . (m9aa1 + 1) by A26, A36, A38, Lm15, JORDAN12:2;

then Wn . (Wn1 .rfind m) = Wn . m by A20, A27, A33, A36, A39, Lm15, JORDAN12:2;

then Wn1 .rfind m <= m by A9, A27, A34, Def22;

hence Wn1 .rfind m = m by A21, XXREAL_0:1; :: thesis: verum

end;A36: 1 <= Wn1 .rfind m by ABIAN:12;

A37: m9aa1 < (Wn1 .rfind m) - 0 by XREAL_1:15;

then A38: m9aa1 < len (Wn1 .cut (1,(Wn1 .rfind m))) by A26, Lm22;

A39: m9aa1 < len (Wn .cut (1,(Wn1 .rfind m))) by A8, A26, A37, Lm22, XXREAL_0:2;

Wn1 .rfind m < len (Wn .cut (1,(Wn .find ((2 * n) + 1)))) by A14, A35, Lm22;

then Wn1 .cut (1,(Wn1 .rfind m)) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,(Wn1 .rfind m)) by A25, A23, A36, Lm21, JORDAN12:2

.= Wn .cut (1,(Wn1 .rfind m)) by A35, Lm20 ;

then Wn1 . (Wn1 .rfind m) = (Wn .cut (1,(Wn1 .rfind m))) . (m9aa1 + 1) by A26, A36, A38, Lm15, JORDAN12:2;

then Wn . (Wn1 .rfind m) = Wn . m by A20, A27, A33, A36, A39, Lm15, JORDAN12:2;

then Wn1 .rfind m <= m by A9, A27, A34, Def22;

hence Wn1 .rfind m = m by A21, XXREAL_0:1; :: thesis: verum

suppose A40:
Wn .find ((2 * n) + 1) <= Wn1 .rfind m
; :: thesis: Wn1 .rfind m = m

set x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1));

A41: Wn1 . (Wn1 .rfind m) = Wn . (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) by A13, A22, A18, A24, A26, A40, Lm30;

A42: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= len Wn by A13, A22, A18, A24, A26, A40, Lm30;

(Wn1 .rfind m) + (Wn .find ((2 * n) + 1)) <= (Wn1 .rfind m) + (Wn .rfind ((2 * n) + 1)) by A24, XREAL_1:7;

then A43: ((Wn1 .rfind m) + (Wn .find ((2 * n) + 1))) - (Wn .find ((2 * n) + 1)) <= ((Wn1 .rfind m) + (Wn .rfind ((2 * n) + 1))) - (Wn .find ((2 * n) + 1)) by XREAL_1:13;

reconsider x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) as Element of NAT by A13, A22, A18, A24, A26, A40, Lm30;

x <= m by A9, A20, A34, A33, A41, A42, Def22;

then Wn1 .rfind m <= m by A43, XXREAL_0:2;

hence Wn1 .rfind m = m by A21, XXREAL_0:1; :: thesis: verum

end;A41: Wn1 . (Wn1 .rfind m) = Wn . (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) by A13, A22, A18, A24, A26, A40, Lm30;

A42: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= len Wn by A13, A22, A18, A24, A26, A40, Lm30;

(Wn1 .rfind m) + (Wn .find ((2 * n) + 1)) <= (Wn1 .rfind m) + (Wn .rfind ((2 * n) + 1)) by A24, XREAL_1:7;

then A43: ((Wn1 .rfind m) + (Wn .find ((2 * n) + 1))) - (Wn .find ((2 * n) + 1)) <= ((Wn1 .rfind m) + (Wn .rfind ((2 * n) + 1))) - (Wn .find ((2 * n) + 1)) by XREAL_1:13;

reconsider x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) as Element of NAT by A13, A22, A18, A24, A26, A40, Lm30;

x <= m by A9, A20, A34, A33, A41, A42, Def22;

then Wn1 .rfind m <= m by A43, XXREAL_0:2;

hence Wn1 .rfind m = m by A21, XXREAL_0:1; :: thesis: verum

suppose A44:
m = (2 * n) + 1
; :: thesis: Wn1 .rfind m = m

then
m <= len (Wn .cut (1,(Wn .find ((2 * n) + 1))))
by A11, A17, Lm22;

then A45: Wn1 .cut (1,m) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,m) by A25, A19, A23, Lm21, JORDAN12:2

.= Wn .cut (1,m) by A10, A17, Lm20 ;

reconsider maa1 = m - 1 as Element of NAT by ABIAN:12, INT_1:5;

A46: maa1 + 1 = m ;

A47: maa1 < m - 0 by XREAL_1:15;

then A48: maa1 < len (Wn .cut (1,m)) by A7, A8, Lm22, XXREAL_0:2;

maa1 < len (Wn1 .cut (1,m)) by A7, A47, Lm22;

then Wn1 . m = (Wn .cut (1,m)) . m by A7, A19, A45, A46, Lm15, JORDAN12:2;

then A49: Wn1 . m = Wn . m by A9, A19, A46, A48, Lm15, JORDAN12:2;

end;then A45: Wn1 .cut (1,m) = (Wn .cut (1,(Wn .find ((2 * n) + 1)))) .cut (1,m) by A25, A19, A23, Lm21, JORDAN12:2

.= Wn .cut (1,m) by A10, A17, Lm20 ;

reconsider maa1 = m - 1 as Element of NAT by ABIAN:12, INT_1:5;

A46: maa1 + 1 = m ;

A47: maa1 < m - 0 by XREAL_1:15;

then A48: maa1 < len (Wn .cut (1,m)) by A7, A8, Lm22, XXREAL_0:2;

maa1 < len (Wn1 .cut (1,m)) by A7, A47, Lm22;

then Wn1 . m = (Wn .cut (1,m)) . m by A7, A19, A45, A46, Lm15, JORDAN12:2;

then A49: Wn1 . m = Wn . m by A9, A19, A46, A48, Lm15, JORDAN12:2;

now :: thesis: not m < Wn1 .rfind m

hence
Wn1 .rfind m = m
by A21, XXREAL_0:1; :: thesis: verumset x = ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1));

assume A50: m < Wn1 .rfind m ; :: thesis: contradiction

then A51: Wn .find ((2 * n) + 1) < Wn1 .rfind m by A12, A15, A44, XXREAL_0:1;

then A52: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) is Element of NAT by A13, A22, A18, A24, A26, Lm30;

A53: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= len Wn by A13, A22, A18, A24, A26, A51, Lm30;

Wn1 . (Wn1 .rfind m) = Wn . (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) by A13, A22, A18, A24, A26, A51, Lm30;

then ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= Wn .rfind ((2 * n) + 1) by A11, A20, A44, A49, A52, A53, Def22;

then (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) - (Wn .rfind ((2 * n) + 1)) <= (Wn .rfind ((2 * n) + 1)) - (Wn .rfind ((2 * n) + 1)) by XREAL_1:13;

then ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .find ((2 * n) + 1)) <= 0 + (Wn .find ((2 * n) + 1)) by XREAL_1:7;

hence contradiction by A12, A15, A44, A50, XXREAL_0:1; :: thesis: verum

end;assume A50: m < Wn1 .rfind m ; :: thesis: contradiction

then A51: Wn .find ((2 * n) + 1) < Wn1 .rfind m by A12, A15, A44, XXREAL_0:1;

then A52: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) is Element of NAT by A13, A22, A18, A24, A26, Lm30;

A53: ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= len Wn by A13, A22, A18, A24, A26, A51, Lm30;

Wn1 . (Wn1 .rfind m) = Wn . (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) by A13, A22, A18, A24, A26, A51, Lm30;

then ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1)) <= Wn .rfind ((2 * n) + 1) by A11, A20, A44, A49, A52, A53, Def22;

then (((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .rfind ((2 * n) + 1))) - (Wn .rfind ((2 * n) + 1)) <= (Wn .rfind ((2 * n) + 1)) - (Wn .rfind ((2 * n) + 1)) by XREAL_1:13;

then ((Wn1 .rfind m) - (Wn .find ((2 * n) + 1))) + (Wn .find ((2 * n) + 1)) <= 0 + (Wn .find ((2 * n) + 1)) by XREAL_1:7;

hence contradiction by A12, A15, A44, A50, XXREAL_0:1; :: thesis: verum

S

reconsider W0 = f . 0 as Subwalk of W by A2, Lm70;

for m being odd Element of NAT st m < (2 * 0) + 1 & m <= len W0 holds

W0 .rfind m = m by ABIAN:12;

then A58: S

for n being Nat holds S

then consider P being Subwalk of W such that

P = f . ((len W) + 1) and

A59: len P <= len W and

A60: for m being odd Element of NAT st m < (2 * ((len W) + 1)) + 1 & m <= len P holds

P .rfind m = m ;

take P ; :: thesis: ( P is Trail-like & P is Path-like )

now :: thesis: for m being odd Element of NAT st m <= len P holds

P .rfind m = m

then
P is Path-like
by Lm67;P .rfind m = m

let m be odd Element of NAT ; :: thesis: ( m <= len P implies P .rfind m = m )

assume A61: m <= len P ; :: thesis: P .rfind m = m

(len P) + 0 < (len W) + 1 by A59, XREAL_1:8;

then (len P) + 0 < ((len W) + 1) + ((len W) + 1) by XREAL_1:8;

then (len P) + 0 < (2 * ((len W) + 1)) + 1 by XREAL_1:8;

then m < (2 * ((len W) + 1)) + 1 by A61, XXREAL_0:2;

hence P .rfind m = m by A60, A61; :: thesis: verum

end;assume A61: m <= len P ; :: thesis: P .rfind m = m

(len P) + 0 < (len W) + 1 by A59, XREAL_1:8;

then (len P) + 0 < ((len W) + 1) + ((len W) + 1) by XREAL_1:8;

then (len P) + 0 < (2 * ((len W) + 1)) + 1 by XREAL_1:8;

then m < (2 * ((len W) + 1)) + 1 by A61, XXREAL_0:2;

hence P .rfind m = m by A60, A61; :: thesis: verum

hence ( P is Trail-like & P is Path-like ) ; :: thesis: verum