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