let G be Graph; :: thesis: for v being Element of G holds <*v*> is_vertex_seq_of {}
let v be Element of G; :: thesis: <*v*> is_vertex_seq_of {}
thus len <*v*> = (len {}) + 1 by FINSEQ_1:40; :: according to GRAPH_2:def 6 :: 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