defpred S₁[ Nat] means for G2 being _Graph
for V being finite Subset of (the_Vertices_of G2)
for G1 being addLoops of G2,V st card V = $1 holds
ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card V) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G2 ex e being object st
( p . (n + 1) is addEdge of p . n,v,e,v & v in V & not e in the_Edges_of (p . n) ) ) );
A1: S₁[ 0 ]

let G2 be _Graph; :: thesis:
let V be finite Subset of (the_Vertices_of G2); :: thesis:
let G1 be addLoops of G2,V; :: thesis:
assume card V = 0 ; :: thesis:
then A2: V = {} ;
take p = <*G1*>; :: thesis:
thus p . 1 == G2 by A2, Th21; :: thesis:
thus p . (len p) = p . 1 by FINSEQ_1:40
.= G1 ; :: thesis:
thus len p = (card V) + 1 by A2, FINSEQ_1:40; :: thesis:
let n be Element of dom p; :: thesis:
A3: 1 <= n by FINSEQ_3:25;
assume n <= (len p) - 1 ; :: thesis:
then n <= 1 - 1 by FINSEQ_1:40;
hence ex v being Vertex of G2 ex e being object st
( p . (n + 1) is addEdge of p . n,v,e,v & v in V & not e in the_Edges_of (p . n) ) by A3, XXREAL_0:2; :: thesis:

end;

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

proof

let k be Nat; :: thesis:
assume A5: S₁[k] ; :: thesis:
let G2 be _Graph; :: thesis:
let V be finite Subset of (the_Vertices_of G2); :: thesis:
let G1 be addLoops of G2,V; :: thesis:
assume A6: card V = k + 1 ; :: thesis:
then A7: V <> {} ;
set v0 = the Element of V;
the Element of V in V by A7;
then reconsider v0 = the Element of V as Vertex of G2 ;
reconsider V9 = V \ {v0} as finite Subset of (the_Vertices_of G2) ;
A8: V = V9 \/ {v0} by A7, ZFMISC_1:116;
reconsider V0 = {v0} as finite Subset of (the_Vertices_of G2) ;
v0 in {v0} by TARSKI:def 1;
then A9: not v0 in V9 by XBOOLE_0:def 5;
then V9 misses V0 by ZFMISC_1:50;
then consider G9 being addLoops of G2,V9 such that
A10: G1 is addLoops of G9,V0 by A8, Th24;
card V9 = (card V) - (card V0) by A7, ZFMISC_1:31, CARD_2:44
.= (k + 1) - 1 by A6, CARD_1:30 ;
then consider p being non empty Graph-yielding FinSequence such that
A11: ( p . 1 == G2 & p . (len p) = G9 & len p = (card V9) + 1 ) and
A12: for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G2 ex e being object st
( p . (n + 1) is addEdge of p . n,v,e,v & v in V9 & not e in the_Edges_of (p . n) ) by A5;
take q = p ^ <*G1*>; :: thesis:
1 <= len p by FINSEQ_1:20;
then 1 in dom p by FINSEQ_3:25;
hence q . 1 == G2 by A11, FINSEQ_1:def 7; :: thesis:
A13: len q = (len p) + (len <*G1*>) by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
hence A14: q . (len q) = G1 by FINSEQ_1:42; :: thesis:
thus len q = (card V) + 1 by A8, A9, A11, A13, CARD_2:41; :: thesis:
let n be Element of dom q; :: thesis:
assume n <= (len q) - 1 ; :: thesis:

per cases by Lm2;

suppose A15: n = (len q) - 1 ; :: thesis:

then A16: q . (n + 1) = G1 by A14;
A17: 1 <= n by FINSEQ_3:25;
A18: n = len p by A13, A15;
then n in dom p by A17, FINSEQ_3:25;
then A19: q . n = G9 by A11, A18, FINSEQ_1:def 7;
v0 is Vertex of G9 by Th15;
then consider e being object such that
A20: ( not e in the_Edges_of G9 & G1 is addEdge of G9,v0,e,v0 ) by A10, Th27;
reconsider v0 = v0 as Vertex of G2 ;
take v0 ; :: thesis:
take e ; :: thesis:
thus q . (n + 1) is addEdge of q . n,v0,e,v0 by A16, A19, A20; :: thesis:
thus v0 in V by A7; :: thesis:
thus not e in the_Edges_of (q . n) by A19, A20; :: thesis:

end;

suppose A21: n <= (len p) - 1 ; :: thesis:

then A22: 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 A22, FINSEQ_3:25;
consider v being Vertex of G2, e being object such that
A23: ( p . (m + 1) is addEdge of p . m,v,e,v & v in V9 & not e in the_Edges_of (p . m) ) by A12, A21;
( 1 + 0 <= n + 1 & n + 1 <= ((len p) - 1) + 1 ) by A21, XREAL_1:6;
then n + 1 in dom p by FINSEQ_3:25;
then A24: q . (n + 1) = p . (m + 1) by FINSEQ_1:def 7;
A25: q . n = p . m by FINSEQ_1:def 7;
take v ; :: thesis:
take e ; :: thesis:
v in V by A23, XBOOLE_1:36, TARSKI:def 3;
hence ( q . (n + 1) is addEdge of q . n,v,e,v & v in V & not e in the_Edges_of (q . n) ) by A23, A24, A25; :: thesis:

end;

A26: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A4);
let G2 be _Graph; :: thesis:
let V be finite Subset of (the_Vertices_of G2); :: thesis:
let G1 be addLoops of G2,V; :: thesis:
thus ex p being non empty Graph-yielding FinSequence st
( p . 1 == G2 & p . (len p) = G1 & len p = (card V) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being Vertex of G2 ex e being object st
( p . (n + 1) is addEdge of p . n,v,e,v & v in V & not e in the_Edges_of (p . n) ) ) ) by A26; :: thesis: