let G1, G2 be _Graph; :: thesis: for W1 being Walk of G1
for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
( len W1 = len W2 & W1 .length() = W2 .length() & W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )
let W1 be Walk of G1; :: thesis: for W2 being Walk of G2 st W1 .vertexSeq() = W2 .vertexSeq() holds
( len W1 = len W2 & W1 .length() = W2 .length() & W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )
let W2 be Walk of G2; :: thesis: ( W1 .vertexSeq() = W2 .vertexSeq() implies ( len W1 = len W2 & W1 .length() = W2 .length() & W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() ) )
assume A1: W1 .vertexSeq() = W2 .vertexSeq() ; :: thesis: ( len W1 = len W2 & W1 .length() = W2 .length() & W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )
hence len W1 = len W2 by Lm3; :: thesis: ( W1 .length() = W2 .length() & W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )
hence W1 .length() = W2 .length() by Lm2; :: thesis: ( W1 .first() = W2 .first() & W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )
thus A2: W1 .first() = W1 . 1 by GLIB_001:def 6
.= W2 . 1 by A1, Th29, POLYFORM:4
.= W2 .first() by GLIB_001:def 6 ; :: thesis: ( W1 .last() = W2 .last() & W2 is_Walk_from W1 .first() ,W1 .last() )
thus W1 .last() = W1 . (len W1) by GLIB_001:def 7
.= W1 . (len W2) by A1, Lm3
.= W2 . (len W2) by A1, Th29
.= W2 .last() by GLIB_001:def 7 ; :: thesis: W2 is_Walk_from W1 .first() ,W1 .last()
hence W2 is_Walk_from W1 .first() ,W1 .last() by A2, GLIB_001:def 23; :: thesis: verum