let p be Path of G; :: thesis: ( p is empty implies p is cyclic )
assume A1: p is empty ; :: thesis: p is cyclic
consider x being Vertex of G;
A2: 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 x9, y9 being Vertex of G st
( x9 = <*x*> . n & y9 = <*x*> . (n + 1) & p . n joins x9,y9 ) ) & <*x*> . 1 = <*x*> . (len <*x*>) )
thus len <*x*> = (len p) + 1 by A1, CARD_1:47, FINSEQ_1:56; :: 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 x9, y9 being Vertex of G st
( x9 = <*x*> . n & y9 = <*x*> . (n + 1) & p . n joins x9,y9 ) ) & <*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 x9, y9 being Vertex of G st
( x9 = <*x*> . n & y9 = <*x*> . (n + 1) & p . n joins x9,y9 ) ) & <*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 that
A3: 1 <= n and
A4: n <= len <*x*> ; :: thesis: <*x*> . n in the carrier of G
A5: n <= 1 by A4, FINSEQ_1:56;
A6: n = 1 by A3, A5, XXREAL_0:1;
thus <*x*> . n in the carrier of G by A2, A6, FINSEQ_1:57; :: thesis: verum

end;

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