set IT = <*> (the_Edges_of G);
set vs = <*(choose (the_Vertices_of G))*>;
reconsider vs = <*(choose (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 ) )
len vs = 0 + 1 by FINSEQ_1:57;
hence len vs = (len (<*> (the_Edges_of G))) + 1 ; :: 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 ( 1 <= n & n <= len (<*> (the_Edges_of G)) ) ; :: thesis: (<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G
hence (<*> (the_Edges_of G)) . n Joins vs . n,vs . (n + 1),G ; :: thesis: verum