let G2 be _Graph; :: thesis: for V being finite set
for G1 being addVertices of G2,V ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
defpred S₁[ Nat] means for V being finite set
for G1 being addVertices of G2,V st card (V \ (the_Vertices_of G2)) = $1 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) );
A1: S₁[ 0 ]

proof

let V be finite set ; :: thesis: for G1 being addVertices of G2,V st card (V \ (the_Vertices_of G2)) = 0 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
let G1 be addVertices of G2,V; :: thesis: ( card (V \ (the_Vertices_of G2)) = 0 implies ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) ) )
assume A2: card (V \ (the_Vertices_of G2)) = 0 ; :: thesis: ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
then V \ (the_Vertices_of G2) = {} ;
then A3: G1 == G2 by XBOOLE_1:37, GLIB_006:78;
reconsider p = <*G1*> as non empty Graph-yielding FinSequence ;
take p ; :: thesis: ( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
thus p . 1 == G2 by A3; :: thesis: ( p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
thus p . (len p) = p . 1 by FINSEQ_1:40
.= G1 ; :: thesis: ( len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
thus len p = (card (V \ (the_Vertices_of G2))) + 1 by A2, FINSEQ_1:40; :: thesis: for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) )
let n be Element of dom p; :: thesis: ( n <= (len p) - 1 implies ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) )
( 1 <= n & n <= len p ) by FINSEQ_3:25;
then ( 1 <= n & n <= 1 ) by FINSEQ_1:40;
then A4: n = 1 by XXREAL_0:1;
assume n <= (len p) - 1 ; :: thesis: ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) )
then n <= 1 - 1 by FINSEQ_1:40;
hence ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) by A4; :: thesis: verum

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]
let V be finite set ; :: thesis: for G1 being addVertices of G2,V st card (V \ (the_Vertices_of G2)) = k + 1 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
let G1 be addVertices of G2,V; :: thesis: ( card (V \ (the_Vertices_of G2)) = k + 1 implies ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) ) )
assume A7: card (V \ (the_Vertices_of G2)) = k + 1 ; :: thesis: ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) )
then A8: V \ (the_Vertices_of G2) <> {} ;
set v0 = the Element of V \ (the_Vertices_of G2);
set V0 = V \ { the Element of V \ (the_Vertices_of G2)};
set G3 = the addVertices of G2,V \ { the Element of V \ (the_Vertices_of G2)};
(V \ { the Element of V \ (the_Vertices_of G2)}) \ (the_Vertices_of G2) = (V \ { the Element of V \ (the_Vertices_of G2)}) \ ((V \ { the Element of V \ (the_Vertices_of G2)}) /\ (the_Vertices_of G2)) by XBOOLE_1:47;
then A9: card ((V \ { the Element of V \ (the_Vertices_of G2)}) \ (the_Vertices_of G2)) = (card (V \ { the Element of V \ (the_Vertices_of G2)})) - (card ((V \ { the Element of V \ (the_Vertices_of G2)}) /\ (the_Vertices_of G2))) by CARD_2:44, XBOOLE_1:17;
A10: the Element of V \ (the_Vertices_of G2) in V by A8, XBOOLE_0:def 5;
then A11: card (V \ { the Element of V \ (the_Vertices_of G2)}) = (card V) - (card { the Element of V \ (the_Vertices_of G2)}) by CARD_2:44, ZFMISC_1:31
.= (card V) - 1 by CARD_1:30 ;
A12: not the Element of V \ (the_Vertices_of G2) in the_Vertices_of G2 by A8, XBOOLE_0:def 5;
then the_Vertices_of G2 misses { the Element of V \ (the_Vertices_of G2)} by ZFMISC_1:50;
then (the_Vertices_of G2) /\ ({ the Element of V \ (the_Vertices_of G2)} \/ (V \ { the Element of V \ (the_Vertices_of G2)})) = (the_Vertices_of G2) /\ (V \ { the Element of V \ (the_Vertices_of G2)}) by XBOOLE_1:78;
then (the_Vertices_of G2) /\ (V \ { the Element of V \ (the_Vertices_of G2)}) = (the_Vertices_of G2) /\ V by A10, ZFMISC_1:116;
then A13: card ((V \ { the Element of V \ (the_Vertices_of G2)}) \ (the_Vertices_of G2)) = ((card V) - (card (V /\ (the_Vertices_of G2)))) - 1 by A9, A11
.= (card (V \ (V /\ (the_Vertices_of G2)))) - 1 by CARD_2:44, XBOOLE_1:17
.= (card (V \ (the_Vertices_of G2))) - 1 by XBOOLE_1:47
.= k by A7 ;
then consider p being non empty Graph-yielding FinSequence such that
A14: ( p . 1 == G2 & p . (len p) = the addVertices of G2,V \ { the Element of V \ (the_Vertices_of G2)} & len p = (card ((V \ { the Element of V \ (the_Vertices_of G2)}) \ (the_Vertices_of G2))) + 1 ) and
A15: for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of the addVertices of G2,V \ { the Element of V \ (the_Vertices_of G2)} st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) by A6;
reconsider q = p ^ <*G1*> as non empty Graph-yielding FinSequence ;
take q ; :: thesis: ( q . 1 == G2 & q . (len q) = G1 & len q = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom q st n <= (len q) - 1 holds
ex v being Vertex of G1 st
( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) ) ) )
1 in dom p by FINSEQ_5:6;
hence q . 1 == G2 by A14, FINSEQ_1:def 7; :: thesis: ( q . (len q) = G1 & len q = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom q st n <= (len q) - 1 holds
ex v being Vertex of G1 st
( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) ) ) )
A16: len q = (len p) + (len <*G1*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
hence A17: q . (len q) = G1 by FINSEQ_1:42; :: thesis: ( len q = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom q st n <= (len q) - 1 holds
ex v being Vertex of G1 st
( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) ) ) )
thus len q = (card (V \ (the_Vertices_of G2))) + 1 by A7, A13, A14, A16; :: thesis: for n being Element of dom q st n <= (len q) - 1 holds
ex v being Vertex of G1 st
( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) )
G1 is addVertices of G2,{ the Element of V \ (the_Vertices_of G2)} \/ (V \ { the Element of V \ (the_Vertices_of G2)}) by A10, ZFMISC_1:116;
then consider G4 being addVertices of G2,V \ { the Element of V \ (the_Vertices_of G2)} such that
A18: G1 is addVertices of G4,{ the Element of V \ (the_Vertices_of G2)} by GLIB_006:83;
A19: G1 is addVertices of the addVertices of G2,V \ { the Element of V \ (the_Vertices_of G2)},{ the Element of V \ (the_Vertices_of G2)} by A18, Th32, GLIB_006:77;
let n be Element of dom q; :: thesis: ( n <= (len q) - 1 implies ex v being Vertex of G1 st
( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) ) )
assume n <= (len q) - 1 ; :: thesis: ex v being Vertex of G1 st
( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) )

per cases then ( n = (len q) - 1 or n <= (len p) - 1 ) by Lm12;

suppose A20: n = (len q) - 1 ; :: thesis: ex v being Vertex of G1 st
( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) )

then A21: q . (n + 1) = G1 by A17;
1 <= n by FINSEQ_3:25;
then n in dom p by A16, A20, FINSEQ_3:25;
then A24: q . n = the addVertices of G2,V \ { the Element of V \ (the_Vertices_of G2)} by A14, A16, A20, FINSEQ_1:def 7;
the_Vertices_of G1 = (the_Vertices_of G2) \/ V by GLIB_006:def 10;
then reconsider v0 = the Element of V \ (the_Vertices_of G2) as Vertex of G1 by A10, TARSKI:def 3, XBOOLE_1:7;
take v0 ; :: thesis: ( q . (n + 1) is addVertex of q . n,v0 & not v0 in the_Vertices_of (q . n) )
thus q . (n + 1) is addVertex of q . n,v0 by A19, A21, A24; :: thesis: not v0 in the_Vertices_of (q . n)
v0 in {v0} by TARSKI:def 1;
then not v0 in V \ { the Element of V \ (the_Vertices_of G2)} by XBOOLE_0:def 5;
then not v0 in (the_Vertices_of G2) \/ (V \ { the Element of V \ (the_Vertices_of G2)}) by A12, XBOOLE_0:def 3;
hence not v0 in the_Vertices_of (q . n) by A24, GLIB_006:def 10; :: thesis: verum

end;

suppose A25: n <= (len p) - 1 ; :: thesis: ex v being Vertex of G1 st
( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) )

then A26: n + 0 <= ((len p) - 1) + 1 by XREAL_1:7;
1 <= n by FINSEQ_3:25;
then reconsider m = n as Element of dom p by A26, FINSEQ_3:25;
consider v being Vertex of the addVertices of G2,V \ { the Element of V \ (the_Vertices_of G2)} such that
A27: ( p . (m + 1) is addVertex of p . m,v & not v in the_Vertices_of (p . m) ) by A15, A25;
( 1 + 0 <= n + 1 & n + 1 <= ((len p) - 1) + 1 ) by A25, XREAL_1:6;
then n + 1 in dom p by FINSEQ_3:25;
then A28: q . (n + 1) = p . (m + 1) by FINSEQ_1:def 7;
A29: q . n = p . m by FINSEQ_1:def 7;
the_Vertices_of the addVertices of G2,V \ { the Element of V \ (the_Vertices_of G2)} c= the_Vertices_of G1 by A19, GLIB_006:def 9;
then reconsider v = v as Vertex of G1 by TARSKI:def 3;
take v ; :: thesis: ( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) )
thus ( q . (n + 1) is addVertex of q . n,v & not v in the_Vertices_of (q . n) ) by A27, A28, A29; :: thesis: verum

end;

end;

end;

A30: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
thus for V being finite set
for G1 being addVertices of G2,V ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card (V \ (the_Vertices_of G2))) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G1 st
( p . (n + 1) is addVertex of p . n,v & not v in the_Vertices_of (p . n) ) ) ) by A30; :: thesis: verum