let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() holds

W1 = W2

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() holds

W1 = W2

let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() implies W1 = W2 )

assume A1: ( W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() ) ; :: thesis: W1 = W2

A2: (len W1) + 1 = 2 * (len (W2 .vertexSeq())) by A1, GLIB_001:def 14

.= (len W2) + 1 by GLIB_001:def 14 ;

for n being Nat st 1 <= n & n <= len W1 holds

W1 . n = W2 . n

for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() holds

W1 = W2

let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() holds

W1 = W2

let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() implies W1 = W2 )

assume A1: ( W1 .vertexSeq() = W2 .vertexSeq() & W1 .edgeSeq() = W2 .edgeSeq() ) ; :: thesis: W1 = W2

A2: (len W1) + 1 = 2 * (len (W2 .vertexSeq())) by A1, GLIB_001:def 14

.= (len W2) + 1 by GLIB_001:def 14 ;

for n being Nat st 1 <= n & n <= len W1 holds

W1 . n = W2 . n

proof

hence
W1 = W2
by A2, FINSEQ_1:def 17; :: thesis: verum
let n be Nat; :: thesis: ( 1 <= n & n <= len W1 implies W1 . n = W2 . n )

assume A3: ( 1 <= n & n <= len W1 ) ; :: thesis: W1 . n = W2 . n

end;assume A3: ( 1 <= n & n <= len W1 ) ; :: thesis: W1 . n = W2 . n

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

end;

suppose
n is odd
; :: thesis: W1 . n = W2 . n

then reconsider m = n as odd Element of NAT by ORDINAL1:def 12;

thus W1 . n = W1 .vertexAt m by A3, GLIB_001:def 8

.= (W1 .vertexSeq()) . ((m + 1) div 2) by A3, GLIB_001:72

.= W2 .vertexAt m by A1, A2, A3, GLIB_001:72

.= W2 . n by A2, A3, GLIB_001:def 8 ; :: thesis: verum

end;thus W1 . n = W1 .vertexAt m by A3, GLIB_001:def 8

.= (W1 .vertexSeq()) . ((m + 1) div 2) by A3, GLIB_001:72

.= W2 .vertexAt m by A1, A2, A3, GLIB_001:72

.= W2 . n by A2, A3, GLIB_001:def 8 ; :: thesis: verum

suppose
n is even
; :: thesis: W1 . n = W2 . n

then reconsider m = n as even Element of NAT by ORDINAL1:def 12;

thus W1 . n = (W1 .edgeSeq()) . (m div 2) by A3, GLIB_001:77

.= W2 . n by A1, A2, A3, GLIB_001:77 ; :: thesis: verum

end;thus W1 . n = (W1 .edgeSeq()) . (m div 2) by A3, GLIB_001:77

.= W2 . n by A1, A2, A3, GLIB_001:77 ; :: thesis: verum