let p be Path of G; :: thesis: ( p is empty implies p is cyclic )
assume A1: p is empty ; :: thesis: p is cyclic
set x = the Vertex of G;
take <* the Vertex of G*> ; :: according to GRAPH_1:def 17 :: thesis: ( len <* the Vertex of G*> = (len p) + 1 & ( for n being Nat st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) )
thus len <* the Vertex of G*> = (len p) + 1 by A1, FINSEQ_1:39; :: thesis: ( ( for n being Nat st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) )
thus for n being Nat st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G :: thesis: ( ( for n being Nat st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) ) & <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) )

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len <* the Vertex of G*> implies <* the Vertex of G*> . n in the carrier of G )
assume that
A3: 1 <= n and
A4: n <= len <* the Vertex of G*> ; :: thesis: <* the Vertex of G*> . n in the carrier of G
n <= 1 by A4, FINSEQ_1:39;
then n = 1 by A3, XXREAL_0:1;
hence <* the Vertex of G*> . n in the carrier of G ; :: thesis: verum

end;

thus for n being Nat st 1 <= n & n <= len p holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & p . n joins x9,y9 ) by A1; :: thesis: <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>)
thus <* the Vertex of G*> . 1 = <* the Vertex of G*> . (len <* the Vertex of G*>) by FINSEQ_1:39; :: thesis: verum