let G be _Graph; for W1, W2 being Walk of G st W1 is_a_prefix_of W2 holds
W1 .edges() c= W2 .edges()
let W1, W2 be Walk of G; ( W1 is_a_prefix_of W2 implies W1 .edges() c= W2 .edges() )
assume A1:
W1 c= W2
; W1 .edges() c= W2 .edges()
let x be object ; TARSKI:def 3 ( not x in W1 .edges() or x in W2 .edges() )
assume
x in W1 .edges()
; x in W2 .edges()
then consider n being even Element of NAT such that
A2:
1 <= n
and
A3:
n <= len W1
and
A4:
W1 . n = x
by GLIB_001:99;
n in dom W1
by A2, A3, FINSEQ_3:25;
then A5:
W2 . n = x
by A1, A4, GRFUNC_1:2;
len W1 <= len W2
by A1, FINSEQ_1:63;
then
n <= len W2
by A3, XXREAL_0:2;
hence
x in W2 .edges()
by A2, A5, GLIB_001:99; verum