let G be Graph; :: thesis: for v being Element of the carrier of G holds <*v*> is_oriented_vertex_seq_of {}
let v be Element of the carrier of G; :: thesis: <*v*> is_oriented_vertex_seq_of {}
set c = {} ;
thus len <*v*> = (len {} ) + 1 by FINSEQ_1:57; :: according to GRAPH_4:def 5 :: thesis: for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1)
let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len {} implies {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) )
assume ( 1 <= n & n <= len {} ) ; :: thesis: {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1)
hence {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) ; :: thesis: verum