let G be connected Graph; for p being Path of G
for vs being FinSequence of the carrier of G st p is Eulerian & vs is_vertex_seq_of p holds
rng vs = the carrier of G
let p be Path of G; for vs being FinSequence of the carrier of G st p is Eulerian & vs is_vertex_seq_of p holds
rng vs = the carrier of G
let vs be FinSequence of the carrier of G; ( p is Eulerian & vs is_vertex_seq_of p implies rng vs = the carrier of G )
assume that
A1:
p is Eulerian
and
A2:
vs is_vertex_seq_of p
and
A3:
rng vs <> the carrier of G
; contradiction
consider x being object such that
A4:
( ( x in rng vs & not x in the carrier of G ) or ( x in the carrier of G & not x in rng vs ) )
by A3, TARSKI:2;
vs <> {}
by A2;
then consider y being object such that
A5:
y in rng vs
by XBOOLE_0:def 1;
A6:
rng vs c= the carrier of G
by FINSEQ_1:def 4;
then consider c being Chain of G, vs1 being FinSequence of the carrier of G such that
A7:
not c is empty
and
A8:
( vs1 is_vertex_seq_of c & vs1 . 1 = x )
and
vs1 . (len vs1) = y
by A4, A5, Th18;
A9:
1 <= len c
by A7, NAT_1:14;
A10:
rng p = the carrier' of G
by A1;
reconsider c = c as FinSequence of the carrier' of G by MSSCYC_1:def 1;
1 in dom c
by A9, FINSEQ_3:25;
then
c . 1 in the carrier' of G
by PARTFUN1:4;
then
( the Target of G . (c . 1) in rng vs & the Source of G . (c . 1) in rng vs )
by A2, A10, Th15;
hence
contradiction
by A6, A4, A8, A9, Lm3; verum