let G be _Graph; :: thesis: for W being Walk of G

for S being Subwalk of W st S .first() = W .first() & S .edgeSeq() = W .edgeSeq() holds

S = W

let W be Walk of G; :: thesis: for S being Subwalk of W st S .first() = W .first() & S .edgeSeq() = W .edgeSeq() holds

S = W

let S be Subwalk of W; :: thesis: ( S .first() = W .first() & S .edgeSeq() = W .edgeSeq() implies S = W )

assume that

A1: S .first() = W .first() and

A2: S .edgeSeq() = W .edgeSeq() ; :: thesis: S = W

defpred S_{1}[ Nat] means ( $1 in dom S implies S . $1 = W . $1 );

len S = (2 * (len (W .edgeSeq()))) + 1 by A2, GLIB_001:def 15;

then A3: len S = len W by GLIB_001:def 15;

_{1}[n]
from NAT_1:sch 4(A4);

for k being Nat st 1 <= k & k <= len S holds

S . k = W . k by A18, FINSEQ_3:25;

hence S = W by A3, FINSEQ_1:14; :: thesis: verum

for S being Subwalk of W st S .first() = W .first() & S .edgeSeq() = W .edgeSeq() holds

S = W

let W be Walk of G; :: thesis: for S being Subwalk of W st S .first() = W .first() & S .edgeSeq() = W .edgeSeq() holds

S = W

let S be Subwalk of W; :: thesis: ( S .first() = W .first() & S .edgeSeq() = W .edgeSeq() implies S = W )

assume that

A1: S .first() = W .first() and

A2: S .edgeSeq() = W .edgeSeq() ; :: thesis: S = W

defpred S

len S = (2 * (len (W .edgeSeq()))) + 1 by A2, GLIB_001:def 15;

then A3: len S = len W by GLIB_001:def 15;

A4: now :: thesis: for k being Nat st ( for n being Nat st n < k holds

S_{1}[n] ) holds

S_{1}[k]

A18:
for n being Nat holds SS

S

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[b_{1}] )

assume A5: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[b_{1}]

A6: k in NAT by ORDINAL1:def 12;

end;S

assume A5: for n being Nat st n < k holds

S

A6: k in NAT by ORDINAL1:def 12;

per cases
( k in dom S or not k in dom S )
;

end;

suppose A7:
k in dom S
; :: thesis: S_{1}[b_{1}]

then A8:
1 <= k
by FINSEQ_3:25;

A9: k <= len S by A7, FINSEQ_3:25;

end;A9: k <= len S by A7, FINSEQ_3:25;

per cases
( k is even or k is odd )
;

end;

suppose A10:
k is even
; :: thesis: S_{1}[b_{1}]

then
S . k = (S .edgeSeq()) . (k div 2)
by A6, A8, A9, GLIB_001:77;

hence S_{1}[k]
by A2, A3, A8, A9, A10, GLIB_001:77; :: thesis: verum

end;hence S

suppose
k is odd
; :: thesis: S_{1}[b_{1}]

then reconsider kk = k as odd Nat ;

end;per cases
( k = 1 or k > (2 * 0) + 1 )
by A8, XXREAL_0:1;

end;

suppose
k > (2 * 0) + 1
; :: thesis: S_{1}[b_{1}]

then A11:
1 + 2 <= kk
by Th4;

then A12: 3 + (- 2) <= k + (- 2) by XREAL_1:7;

3 + (- 1) <= k + (- 1) by A11, XREAL_1:7;

then 0 <= k - 1 ;

then reconsider k1 = k - 1 as Element of NAT by INT_1:3;

k1 < k by XREAL_1:44;

then A13: k1 <= len S by A9, XXREAL_0:2;

3 + (- 1) <= k + (- 1) by A11, XREAL_1:7;

then 1 <= k1 by XXREAL_0:2;

then k1 in dom S by A13, FINSEQ_3:25;

then A14: S . k1 = W . k1 by A5, XREAL_1:44;

3 + (- 2) <= k + (- 2) by A11, XREAL_1:7;

then reconsider k2 = kk - (2 * 1) as odd Element of NAT by INT_1:3;

A15: k2 < k by XREAL_1:44;

then k2 < len S by A9, XXREAL_0:2;

then A16: S . (k2 + 1) Joins S . k2,S . (k2 + 2),G by GLIB_001:def 3;

k2 <= len S by A9, A15, XXREAL_0:2;

then k2 in dom S by A12, FINSEQ_3:25;

then A17: S . k2 = W . k2 by A5, XREAL_1:44;

k2 < len W by A3, A9, A15, XXREAL_0:2;

then W . (k2 + 1) Joins W . k2,W . (k2 + 2),G by GLIB_001:def 3;

then ( ( S . k2 = S . k2 & S . k = W . k ) or ( S . k2 = W . k & S . k = S . k2 ) ) by A14, A17, A16;

hence S_{1}[k]
; :: thesis: verum

end;then A12: 3 + (- 2) <= k + (- 2) by XREAL_1:7;

3 + (- 1) <= k + (- 1) by A11, XREAL_1:7;

then 0 <= k - 1 ;

then reconsider k1 = k - 1 as Element of NAT by INT_1:3;

k1 < k by XREAL_1:44;

then A13: k1 <= len S by A9, XXREAL_0:2;

3 + (- 1) <= k + (- 1) by A11, XREAL_1:7;

then 1 <= k1 by XXREAL_0:2;

then k1 in dom S by A13, FINSEQ_3:25;

then A14: S . k1 = W . k1 by A5, XREAL_1:44;

3 + (- 2) <= k + (- 2) by A11, XREAL_1:7;

then reconsider k2 = kk - (2 * 1) as odd Element of NAT by INT_1:3;

A15: k2 < k by XREAL_1:44;

then k2 < len S by A9, XXREAL_0:2;

then A16: S . (k2 + 1) Joins S . k2,S . (k2 + 2),G by GLIB_001:def 3;

k2 <= len S by A9, A15, XXREAL_0:2;

then k2 in dom S by A12, FINSEQ_3:25;

then A17: S . k2 = W . k2 by A5, XREAL_1:44;

k2 < len W by A3, A9, A15, XXREAL_0:2;

then W . (k2 + 1) Joins W . k2,W . (k2 + 2),G by GLIB_001:def 3;

then ( ( S . k2 = S . k2 & S . k = W . k ) or ( S . k2 = W . k & S . k = S . k2 ) ) by A14, A17, A16;

hence S

for k being Nat st 1 <= k & k <= len S holds

S . k = W . k by A18, FINSEQ_3:25;

hence S = W by A3, FINSEQ_1:14; :: thesis: verum