take {} ; :: thesis: ( ( for n being Nat st 1 <= n & n <= len {} holds
{} . n in the carrier' of G ) & ex p being FinSequence st
( len p = (len {}) + 1 & ( for n being Nat st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) ) )
thus for n being Nat st 1 <= n & n <= len {} holds
{} . n in the carrier' of G ; :: thesis: ex p being FinSequence st
( len p = (len {}) + 1 & ( for n being Nat st 1 <= n & n <= len p holds
p . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = p . n & y9 = p . (n + 1) & {} . n joins x9,y9 ) ) )
set x = the Vertex of G;
take <* the Vertex of G*> ; :: thesis: ( len <* the Vertex of G*> = (len {}) + 1 & ( for n being Nat st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) )
thus len <* the Vertex of G*> = (len {}) + 1 by FINSEQ_1:39; :: thesis: ( ( for n being Nat st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G ) & ( for n being Nat st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) )
thus for n being Nat st 1 <= n & n <= len <* the Vertex of G*> holds
<* the Vertex of G*> . n in the carrier of G :: thesis: for n being Nat st 1 <= n & n <= len {} holds
ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 )

proof

let n be Nat; :: thesis: ( 1 <= n & n <= len <* the Vertex of G*> implies <* the Vertex of G*> . n in the carrier of G )
assume that
A2: 1 <= n and
A3: n <= len <* the Vertex of G*> ; :: thesis: <* the Vertex of G*> . n in the carrier of G
n <= 1 by A3, FINSEQ_1:39;
then n = 1 by A2, XXREAL_0:1;
hence <* the Vertex of G*> . n in the carrier of G ; :: thesis: verum

end;

let n be Nat; :: thesis: ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) )
thus ( 1 <= n & n <= len {} implies ex x9, y9 being Vertex of G st
( x9 = <* the Vertex of G*> . n & y9 = <* the Vertex of G*> . (n + 1) & {} . n joins x9,y9 ) ) ; :: thesis: verum