let G be Graph; :: thesis: for v being Element of the carrier of G holds <*v*> is_vertex_seq_of {}
let v be Element of the carrier of G; :: thesis: <*v*> is_vertex_seq_of {}
thus len <*v*> = (len {} ) + 1 by FINSEQ_1:57; :: according to GRAPH_2:def 7 :: thesis: for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n joins <*v*> /. n,<*v*> /. (n + 1)
thus for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n joins <*v*> /. n,<*v*> /. (n + 1) ; :: thesis: verum