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₁[ 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;

A4: now :: thesis: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

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 12;

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

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

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

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

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

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

end;

suppose k is odd ; :: thesis: S₁[b₁]

then reconsider kk = k as odd Nat ;

per cases ( k = 1 or k > (2 * 0) + 1 ) by A8, 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 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₁[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;

A18: for n being Nat holds S₁[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