let G be _Graph; for e, x, y being object holds
( e Joins x,y,G iff (G .walkOf (x,e,y)) .edgeSeq() = <*e*> )
let e, x, y be object ; ( e Joins x,y,G iff (G .walkOf (x,e,y)) .edgeSeq() = <*e*> )
set W = G .walkOf (x,e,y);
hereby ( (G .walkOf (x,e,y)) .edgeSeq() = <*e*> implies e Joins x,y,G )
assume A1:
e Joins x,
y,
G
;
(G .walkOf (x,e,y)) .edgeSeq() = <*e*>then
len (G .walkOf (x,e,y)) = 3
by Th13;
then A2:
2
+ 1
= (2 * (len ((G .walkOf (x,e,y)) .edgeSeq()))) + 1
by Def15;
A3:
G .walkOf (
x,
e,
y)
= <*x,e,y*>
by A1, Def5;
A4:
now for k being Nat st 1 <= k & k <= len ((G .walkOf (x,e,y)) .edgeSeq()) holds
((G .walkOf (x,e,y)) .edgeSeq()) . k = <*e*> . klet k be
Nat;
( 1 <= k & k <= len ((G .walkOf (x,e,y)) .edgeSeq()) implies ((G .walkOf (x,e,y)) .edgeSeq()) . k = <*e*> . k )assume that A5:
1
<= k
and A6:
k <= len ((G .walkOf (x,e,y)) .edgeSeq())
;
((G .walkOf (x,e,y)) .edgeSeq()) . k = <*e*> . kA7:
k = 1
by A2, A5, A6, XXREAL_0:1;
then ((G .walkOf (x,e,y)) .edgeSeq()) . k =
(G .walkOf (x,e,y)) . (2 * 1)
by A6, Def15
.=
e
by A3, FINSEQ_1:45
;
hence
((G .walkOf (x,e,y)) .edgeSeq()) . k = <*e*> . k
by A7, FINSEQ_1:def 8;
verum end;
len ((G .walkOf (x,e,y)) .edgeSeq()) = len <*e*>
by A2, FINSEQ_1:39;
hence
(G .walkOf (x,e,y)) .edgeSeq() = <*e*>
by A4, FINSEQ_1:14;
verum
end;
assume
(G .walkOf (x,e,y)) .edgeSeq() = <*e*>
; e Joins x,y,G
then
len ((G .walkOf (x,e,y)) .edgeSeq()) = 1
by FINSEQ_1:39;
then A8:
len (G .walkOf (x,e,y)) = (2 * 1) + 1
by Def15;
hence
e Joins x,y,G
; verum