let G be _Graph; :: thesis: for v being Vertex of G holds
( len (G .walkOf v) = 1 & (G .walkOf v) . 1 = v & (G .walkOf v) .first() = v & (G .walkOf v) .last() = v & G .walkOf v is_Walk_from v,v )
let v be Vertex of G; :: thesis: ( len (G .walkOf v) = 1 & (G .walkOf v) . 1 = v & (G .walkOf v) .first() = v & (G .walkOf v) .last() = v & G .walkOf v is_Walk_from v,v )
thus A1: ( len (G .walkOf v) = 1 & (G .walkOf v) . 1 = v ) by FINSEQ_1:40; :: thesis: ( (G .walkOf v) .first() = v & (G .walkOf v) .last() = v & G .walkOf v is_Walk_from v,v )
thus A2: (G .walkOf v) .first() = v by FINSEQ_1:40; :: thesis: ( (G .walkOf v) .last() = v & G .walkOf v is_Walk_from v,v )
thus (G .walkOf v) .last() = v by A1; :: thesis: G .walkOf v is_Walk_from v,v
hence G .walkOf v is_Walk_from v,v by A2, Def23; :: thesis: verum