let G be WGraph; :: thesis: for W being Walk of G st W is trivial holds
W .weightSeq() = {}
let W be Walk of G; :: thesis: ( W is trivial implies W .weightSeq() = {} )
assume W is trivial ; :: thesis: W .weightSeq() = {}
then W .length() = 0 by GLIB_001:def 26;
then len (W .edgeSeq()) = 0 by GLIB_001:def 18;
then len (W .weightSeq()) = 0 by Def18;
hence W .weightSeq() = {} ; :: thesis: verum