let G be connected Graph; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: contradiction
A4: rng vs c= the carrier of G by FINSEQ_1:def 4;
consider x being set such that
A5: ( ( 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, Th3;
then rng vs <> {} ;
then consider y being set such that
A6: y in rng vs by XBOOLE_0:def 1;
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 and
A9: ( vs1 . 1 = x & vs1 . (len vs1) = y ) by A4, A5, A6, Th23;
len c <> 0 by A7;
then A10: 1 <= len c by NAT_1:14;
reconsider c = c as FinSequence of the carrier' of G by MSSCYC_1:def 1;
1 in dom c by A10, FINSEQ_3:27;
then A11: c . 1 in the carrier' of G by PARTFUN1:27;
rng p = the carrier' of G by A1, Def14;
then ( the Target of G . (c . 1) in rng vs & the Source of G . (c . 1) in rng vs ) by A2, A11, Th20;
hence contradiction by A4, A5, A8, A9, A10, Lm3; :: thesis: verum