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
proof
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
per cases ( n is odd or n is even ) ;
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;
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;
end;
end;
hence W1 = W2 by A2, FINSEQ_1:def 17; :: thesis: verum