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
len S = (2 * (len (W .edgeSeq() ))) + 1 by A2, GLIB_001:def 15;
then A3: len S = len W by GLIB_001:def 15;
defpred S₁[ Nat] means ( $1 in dom S implies S . $1 = W . $1 );

A4: now

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[b₁] )
assume A5: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[b₁]
A6: k in NAT by ORDINAL1:def 13;

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

suppose k in dom S ; :: thesis: S₁[b₁]

then A7: ( 1 <= k & k <= len S ) by FINSEQ_3:27;

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

suppose A8: k is even ; :: thesis: S₁[b₁]

then S . k = (S .edgeSeq() ) . (k div 2) by A6, A7, GLIB_001:78;
hence S₁[k] by A2, A3, A7, A8, GLIB_001:78; :: thesis: verum

end;

suppose not k is even ; :: thesis: S₁[b₁]

then reconsider kk = k as odd Nat ;

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

suppose k = 1 ; :: thesis: S₁[b₁]

hence S₁[k] by A1; :: thesis: verum

end;

suppose k > (2 * 0 ) + 1 ; :: thesis: S₁[b₁]

then A9: 1 + 2 <= kk by Th4;
then ( 0 <= 2 & 3 + (- 1) <= k + (- 1) ) by XREAL_1:9;
then reconsider k1 = k - 1 as Element of NAT by INT_1:16;
( 0 <= 1 & 3 + (- 2) <= k + (- 2) ) by A9, XREAL_1:9;
then reconsider k2 = kk - (2 * 1) as odd Element of NAT by INT_1:16;
3 + (- 1) <= k + (- 1) by A9, XREAL_1:9;
then A10: ( 1 <= k1 & k1 < k ) by XREAL_1:46, XXREAL_0:2;
then k1 <= len S by A7, XXREAL_0:2;
then k1 in dom S by A10, FINSEQ_3:27;
then A11: S . k1 = W . k1 by A5, A10;
A12: 3 + (- 2) <= k + (- 2) by A9, XREAL_1:9;
then A13: ( 1 <= k2 & k2 < k ) by XREAL_1:46;
then k2 <= len S by A7, XXREAL_0:2;
then k2 in dom S by A12, FINSEQ_3:27;
then A14: S . k2 = W . k2 by A5, XREAL_1:46;
( k2 < len S & k2 < len W ) by A3, A7, A13, XXREAL_0:2;
then ( S . (k2 + 1) Joins S . k2,S . (k2 + 2),G & 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 A11, A14, GLIB_000:18;
hence S₁[k] ; :: thesis: verum

end;

end;

end;

end;

end;

suppose not k in dom S ; :: thesis: S₁[b₁]

hence S₁[k] ; :: thesis: verum

end;

end;

end;

A15: for n being Nat holds S₁[n] from NAT_1:sch 4(A4);

now

let k be Nat; :: thesis: ( 1 <= k & k <= len S implies S . k = W . k )
assume A16: ( 1 <= k & k <= len S ) ; :: thesis: S . k = W . k
k in dom S by A16, FINSEQ_3:27;
hence S . k = W . k by A15; :: thesis: verum

end;

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