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 set st x in W .edgeSeq() holds
f . x = x `2 ) ) from FUNCT_1:sch 3();

now

let y be set ; :: 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 set such that
A2: ( x in dom f & f . x = y ) by FUNCT_1:def 5;
A3: ( x in W .edgeSeq() & y = x `2 ) by A1, A2;
consider a, b being set such that
A4: x = [a,b] by A1, A2, RELAT_1:def 1;
y = b by A3, A4, MCART_1:def 2;
then y in rng (W .edgeSeq() ) by A1, A2, A4, RELAT_1:def 5;
hence y in the_Edges_of G ; :: thesis: verum

end;

then A5: rng f c= the_Edges_of G by TARSKI:def 3;

now

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

end;

then f is one-to-one by FUNCT_1:def 8;
then card (W .edgeSeq() ) c= card (the_Edges_of G) by A1, A5, CARD_1:26;
then card (W .edgeSeq() ) <= card (the_Edges_of G) by NAT_1:40;
hence len (W .edgeSeq() ) <= G .size() by GLIB_000:def 27; :: thesis: verum