let G be connected finite Graph; :: thesis: ( ex p being cyclic Path of G st p is Eulerian iff for v being Vertex of G holds Degree v is even )
set E = the carrier' of G;

hereby :: thesis: ( ( for v being Vertex of G holds Degree v is even ) implies ex p being cyclic Path of G st p is Eulerian )

given c being cyclic Path of G such that A1: c is Eulerian ; :: thesis: for v being Vertex of G holds Degree v is even
consider vs being FinSequence of the carrier of G such that
A2: ( vs is_vertex_seq_of c & vs . 1 = vs . (len vs) ) by MSSCYC_1:def 2;
let v be Vertex of G; :: thesis: Degree v is even
A3: rng c = the carrier' of G by A1, Def14;
rng vs = the carrier of G by A1, A2, Th63;
then Degree v,(rng c) is even by A2, Lm4;
hence Degree v is even by A3, Th29; :: thesis: verum

end;

assume A4: for v being Vertex of G holds Degree v is even ; :: thesis: ex p being cyclic Path of G st p is Eulerian

per cases ( G is void or not G is void ) ;

suppose G is void ; :: thesis: ex p being cyclic Path of G st p is Eulerian

then A5: the carrier' of G is empty ;
{} is Element of G -CycleSet by Th56;
then reconsider ec = {} as cyclic Path of G by Def8;
take ec ; :: thesis: ec is Eulerian
thus rng ec = the carrier' of G by A5; :: according to GRAPH_3:def 14 :: thesis: verum

end;

suppose not G is void ; :: thesis: ex p being cyclic Path of G st p is Eulerian

then reconsider G' = G as non void connected finite Graph ;
reconsider V = choose the carrier of G as Vertex of G' ;
choose (the carrier' of G -CycleSet V) in the carrier' of G -CycleSet V ;
then reconsider ec = choose (the carrier' of G -CycleSet V) as Element of G' -CycleSet ;

A6: now

let v be Vertex of G; :: thesis: Degree v,the carrier' of G is even
Degree v = Degree v,the carrier' of G by Th29;
hence Degree v,the carrier' of G is even by A4; :: thesis: verum

end;

Degree V = Degree V,the carrier' of G by Th29;
then A7: Degree V,the carrier' of G <> 0 by Th38;
deffunc H₁( Nat, Element of G' -CycleSet ) -> Element of G' -CycleSet = ExtendCycle $2;
consider f being Function of NAT ,(G' -CycleSet ) such that
A8: ( f . 0 = ec & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 12();

now

assume A9: for n being Element of NAT
for c being Element of G' -CycleSet holds
( not c = f . n or not rng c = the carrier' of G ) ; :: thesis: contradiction
reconsider E = the carrier' of G as finite set by GRAPH_1:def 9;
defpred S₁[ Element of NAT ] means ex c being Element of G' -CycleSet st
( not c is empty & c = f . $1 & $1 <= card (rng c) );
A10: S₁[ 0 ]

proof

take ec ; :: thesis: ( not ec is empty & ec = f . 0 & 0 <= card (rng ec) )
thus not ec is empty by A6, A7, Th60; :: thesis: ( ec = f . 0 & 0 <= card (rng ec) )
thus ec = f . 0 by A8; :: thesis: 0 <= card (rng ec)
thus 0 <= card (rng ec) ; :: thesis: verum

end;

A11: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
given c being Element of G' -CycleSet such that A12: not c is empty and
A13: c = f . n and
A14: n <= card (rng c) ; :: thesis: S₁[n + 1]
reconsider r = ExtendCycle c as Element of G' -CycleSet ;
take r ; :: thesis: ( not r is empty & r = f . (n + 1) & n + 1 <= card (rng r) )
rng c <> E by A9, A13;
hence not r is empty by A4, A12, Th62; :: thesis: ( r = f . (n + 1) & n + 1 <= card (rng r) )
thus r = f . (n + 1) by A8, A13; :: thesis: n + 1 <= card (rng r)
rng c <> E by A9, A13;
then card (rng c) < card (rng r) by A4, A12, Th62;
then n < card (rng r) by A14, XXREAL_0:2;
hence n + 1 <= card (rng r) by NAT_1:13; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A10, A11);
then consider c being Element of G -CycleSet such that
A15: ( not c is empty & c = f . ((card E) + 1) & (card E) + 1 <= card (rng c) ) ;
rng c c= E by FINSEQ_1:def 4;
then card (rng c) <= card E by NAT_1:44;
then (card E) + 1 <= (card E) + 0 by A15, XXREAL_0:2;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then consider n being Element of NAT , c being Element of G -CycleSet such that
A16: ( c = f . n & rng c = the carrier' of G ) ;
reconsider c = c as cyclic Path of G by Def8;
take c ; :: thesis: c is Eulerian
thus rng c = the carrier' of G by A16; :: according to GRAPH_3:def 14 :: thesis: verum

end;

end;