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)
; 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
; ( 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; 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 ; ( 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))
; (<*> (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; verum