let G be _finite _Graph; :: thesis: for W being Trail of G holds len (W .edgeSeq()) <= G .size()
let W be Trail of G; :: thesis: len (W .edgeSeq()) <= G .size()
consider f being Function such that
A1: ( dom f = W .edgeSeq() & ( for x being object st x in W .edgeSeq() holds
f . x = x `2 ) ) from FUNCT_1:sch 3();

now :: thesis: for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2

A2: W .edgeSeq() is one-to-one by Def27;
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; :: thesis: x1 = x2
consider a1, b1 being object such that
A6: x1 = [a1,b1] by A1, A3, RELAT_1:def 1;
A7: a1 in dom (W .edgeSeq()) by A1, A3, A6, FUNCT_1:1;
A8: f . x2 = x2 `2 by A1, A4;
A9: (W .edgeSeq()) . a1 = b1 by A1, A3, A6, FUNCT_1:1;
consider a2, b2 being object such that
A10: x2 = [a2,b2] by A1, A4, RELAT_1:def 1;
A11: a2 in dom (W .edgeSeq()) by A1, A4, A10, FUNCT_1:1;
f . x1 = x1 `2 by A1, A3;
then A12: b1 = f . x1 by A6
.= b2 by A5, A8, A10 ;
then (W .edgeSeq()) . a2 = b1 by A1, A4, A10, FUNCT_1:1;
hence x1 = x2 by A6, A10, A12, A2, A7, A9, A11, FUNCT_1:def 4; :: thesis: verum

end;

then A13: f is one-to-one by FUNCT_1:def 4;

now :: thesis: for y being object st y in rng f holds
y in the_Edges_of G

let y be object ; :: thesis: ( y in rng f implies y in the_Edges_of G )
assume y in rng f ; :: thesis: y in the_Edges_of G
then consider x being object such that
A14: x in dom f and
A15: f . x = y by FUNCT_1:def 3;
consider a, b being object such that
A16: x = [a,b] by A1, A14, RELAT_1:def 1;
y = x `2 by A1, A14, A15;
then y = b by A16;
then y in rng (W .edgeSeq()) by A1, A14, A16, XTUPLE_0:def 13;
hence y in the_Edges_of G ; :: thesis: verum

end;

then rng f c= the_Edges_of G by TARSKI:def 3;
then Segm (card (W .edgeSeq())) c= Segm (card (the_Edges_of G)) by A1, A13, CARD_1:10;
then card (W .edgeSeq()) <= card (the_Edges_of G) by NAT_1:39;
hence len (W .edgeSeq()) <= G .size() by GLIB_000:def 25; :: thesis: verum