let
G
be
_Graph
;
:: thesis:
for
W
being
Walk
of
G
holds
W
.cut
(1,
(
len
W
)
)
=
W
let
W
be
Walk
of
G
;
:: thesis:
W
.cut
(1,
(
len
W
)
)
=
W
1
<=
len
W
by
ABIAN:12
;
then
W
.cut
(1,
(
len
W
)
)
=
(1,
(
len
W
)
)
-cut
W
by
Def11
,
JORDAN12:2
;
hence
W
.cut
(1,
(
len
W
)
)
=
W
by
FINSEQ_6:133
;
:: thesis:
verum