let G be Graph; :: thesis: for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}
let v be Element of G; :: thesis: <*v*> is_oriented_vertex_seq_of {}
set c = {} ;
thus len <*v*> = (len {}) + 1 by FINSEQ_1:40; :: 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 that
A1: 1 <= n and
A2: n <= len {} ; :: thesis: {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1)
thus {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) by A1, A2; :: thesis: verum