let G be _Graph; for x, e, y being object st e Joins x,y,G holds
( (G .walkOf (x,e,y)) .first() = x & (G .walkOf (x,e,y)) .last() = y & G .walkOf (x,e,y) is_Walk_from x,y )
let x, e, y be object ; ( e Joins x,y,G implies ( (G .walkOf (x,e,y)) .first() = x & (G .walkOf (x,e,y)) .last() = y & G .walkOf (x,e,y) is_Walk_from x,y ) )
set W = G .walkOf (x,e,y);
assume
e Joins x,y,G
; ( (G .walkOf (x,e,y)) .first() = x & (G .walkOf (x,e,y)) .last() = y & G .walkOf (x,e,y) is_Walk_from x,y )
then A1:
G .walkOf (x,e,y) = <*x,e,y*>
by Def5;
hence A2:
(G .walkOf (x,e,y)) .first() = x
by FINSEQ_1:45; ( (G .walkOf (x,e,y)) .last() = y & G .walkOf (x,e,y) is_Walk_from x,y )
len (G .walkOf (x,e,y)) = 3
by A1, FINSEQ_1:45;
hence
(G .walkOf (x,e,y)) .last() = y
by A1, FINSEQ_1:45; G .walkOf (x,e,y) is_Walk_from x,y
hence
G .walkOf (x,e,y) is_Walk_from x,y
by A2; verum