let G be _Graph; :: thesis: for T being Trail of G holds T .length() = card (T .edges())
let T be Trail of G; :: thesis: T .length() = card (T .edges())
A1: T .edgeSeq() is one-to-one by GLIB_001:def 27;
thus T .length() = card (dom (T .edgeSeq())) by CARD_1:62
.= card (T .edges()) by A1, CARD_1:70 ; :: thesis: verum