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 S1[ Nat] means ( \$1 in dom S implies S . \$1 = W . \$1 );
len S = (2 * (len ())) + 1 by ;
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
S1[n] ) holds
S1[k]
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S1[n] ) implies S1[b1] )

assume A5: for n being Nat st n < k holds
S1[n] ; :: thesis: S1[b1]
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: S1[b1]
then A8: 1 <= k by FINSEQ_3:25;
A9: k <= len S by ;
per cases ( k is even or k is odd ) ;
suppose k is odd ; :: thesis: S1[b1]
then reconsider kk = k as odd Nat ;
per cases ( k = 1 or k > (2 * 0) + 1 ) by ;
suppose k > (2 * 0) + 1 ; :: thesis: S1[b1]
then A11: 1 + 2 <= kk by Th4;
then A12: 3 + (- 2) <= k + (- 2) by XREAL_1:7;
3 + (- 1) <= k + (- 1) by ;
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 ;
3 + (- 1) <= k + (- 1) by ;
then 1 <= k1 by XXREAL_0:2;
then k1 in dom S by ;
then A14: S . k1 = W . k1 by ;
3 + (- 2) <= k + (- 2) by ;
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 ;
then A16: S . (k2 + 1) Joins S . k2,S . (k2 + 2),G by GLIB_001:def 3;
k2 <= len S by ;
then k2 in dom S by ;
then A17: S . k2 = W . k2 by ;
k2 < len W by ;
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 ;
hence S1[k] ; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
A18: for n being Nat holds S1[n] from for k being Nat st 1 <= k & k <= len S holds
S . k = W . k by ;
hence S = W by ; :: thesis: verum