set IT = <*> (the_Edges_of G);

set vs = <* the Element of the_Vertices_of G*>;

reconsider vs = <* the Element of the_Vertices_of G*> as FinSequence of the_Vertices_of G ;

take <*> (the_Edges_of G) ; :: thesis: ex vs being FinSequence of the_Vertices_of G st

( len vs = (len (<*> (the_Edges_of G))) + 1 & ( for n being Element of NAT st 1 <= n & n <= len (<*> (the_Edges_of G)) holds

(<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G ) )

take vs ; :: thesis: ( len vs = (len (<*> (the_Edges_of G))) + 1 & ( for n being Element of NAT st 1 <= n & n <= len (<*> (the_Edges_of G)) holds

(<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G ) )

thus len vs = (len (<*> (the_Edges_of G))) + 1 by FINSEQ_1:40; :: thesis: for n being Element of NAT st 1 <= n & n <= len (<*> (the_Edges_of G)) holds

(<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (<*> (the_Edges_of G)) implies (<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G )

assume that

A1: 1 <= n and

A2: n <= len (<*> (the_Edges_of G)) ; :: thesis: (<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G

thus (<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G by A1, A2; :: thesis: verum

set vs = <* the Element of the_Vertices_of G*>;

reconsider vs = <* the Element of the_Vertices_of G*> as FinSequence of the_Vertices_of G ;

take <*> (the_Edges_of G) ; :: thesis: ex vs being FinSequence of the_Vertices_of G st

( len vs = (len (<*> (the_Edges_of G))) + 1 & ( for n being Element of NAT st 1 <= n & n <= len (<*> (the_Edges_of G)) holds

(<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G ) )

take vs ; :: thesis: ( len vs = (len (<*> (the_Edges_of G))) + 1 & ( for n being Element of NAT st 1 <= n & n <= len (<*> (the_Edges_of G)) holds

(<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G ) )

thus len vs = (len (<*> (the_Edges_of G))) + 1 by FINSEQ_1:40; :: thesis: for n being Element of NAT st 1 <= n & n <= len (<*> (the_Edges_of G)) holds

(<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G

let n be Element of NAT ; :: thesis: ( 1 <= n & n <= len (<*> (the_Edges_of G)) implies (<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G )

assume that

A1: 1 <= n and

A2: n <= len (<*> (the_Edges_of G)) ; :: thesis: (<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G

thus (<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G by A1, A2; :: thesis: verum