let p be Path of G; :: thesis: ( p is empty implies p is cyclic )
assume Z: p is empty ; :: thesis: p is cyclic
consider x being Vertex of G;
A1: x in the carrier of G ;
take <*x*> ; :: according to GRAPH_1:def 16 :: thesis: ( len <*x*> = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len <*x*> holds
<*x*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds
ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & p . n joins x',y' ) ) & <*x*> . 1 = <*x*> . (len <*x*>) )
thus len <*x*> = (len p) + 1 by CARD_1:47, FINSEQ_1:56, Z; :: thesis: ( ( for n being Element of NAT st 1 <= n & n <= len <*x*> holds
<*x*> . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds
ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & p . n joins x',y' ) ) & <*x*> . 1 = <*x*> . (len <*x*>) )
thus for n being Element of NAT st 1 <= n & n <= len <*x*> holds
<*x*> . n in the carrier of G :: thesis: ( ( for n being Element of NAT st 1 <= n & n <= len p holds
ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & p . n joins x',y' ) ) & <*x*> . 1 = <*x*> . (len <*x*>) )

proof

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len <*x*> implies <*x*> . n in the carrier of G )
assume ( 1 <= n & n <= len <*x*> ) ; :: thesis: <*x*> . n in the carrier of G
then ( 1 <= n & n <= 1 ) by FINSEQ_1:56;
then n = 1 by XXREAL_0:1;
hence <*x*> . n in the carrier of G by A1, FINSEQ_1:57; :: thesis: verum

end;

thus for n being Element of NAT st 1 <= n & n <= len p holds
ex x', y' being Vertex of G st
( x' = <*x*> . n & y' = <*x*> . (n + 1) & p . n joins x',y' ) by Z, CARD_1:47, XXREAL_0:2; :: thesis: <*x*> . 1 = <*x*> . (len <*x*>)
thus <*x*> . 1 = <*x*> . (len <*x*>) by FINSEQ_1:56; :: thesis: verum