set N = card (the_Vertices_of G);
set vs = canFS (the_Vertices_of G);
deffunc H₁( Element of NAT ) -> Element of omega = ((card (the_Vertices_of G)) -' G) + 1;
consider s being sequence of NAT such that
A1: for n being Element of NAT holds s . n = H₁(n) from FUNCT_2:sch 4();
defpred S₁[ object , object ] means ex n being Nat st
( G = n & c₂ = s * (((canFS (the_Vertices_of G)) | (Seg n)) ") );
A2: for n being object st n in NAT holds
ex j being object st S₁[n,j]

proof

let n be object ; :: thesis: ( n in NAT implies ex j being object st S₁[n,j] )
assume n in NAT ; :: thesis: ex j being object st S₁[n,j]
then reconsider n9 = n as Nat ;
take s * (((canFS (the_Vertices_of G)) | (Seg n9)) ") ; :: thesis: S₁[n,s * (((canFS (the_Vertices_of G)) | (Seg n9)) ")]
thus S₁[n,s * (((canFS (the_Vertices_of G)) | (Seg n9)) ")] ; :: thesis: verum

end;

consider S being ManySortedSet of NAT such that
A3: for n being object st n in NAT holds
S₁[n,S . n] from PBOOLE:sch 3(A2);
A4: for n being Nat holds S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) ")

proof

let n be Nat; :: thesis: S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) ")
n in NAT by ORDINAL1:def 12;
then ex i9 being Nat st
( n = i9 & S . n = s * (((canFS (the_Vertices_of G)) | (Seg i9)) ") ) by A3;
hence S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) ") ; :: thesis: verum

end;

A5: for n being Nat st n >= len (canFS (the_Vertices_of G)) holds
S . n = s * ((canFS (the_Vertices_of G)) ")

proof

A6: dom (canFS (the_Vertices_of G)) = Seg (len (canFS (the_Vertices_of G))) by FINSEQ_1:def 3;
let n be Nat; :: thesis: ( n >= len (canFS (the_Vertices_of G)) implies S . n = s * ((canFS (the_Vertices_of G)) ") )
assume n >= len (canFS (the_Vertices_of G)) ; :: thesis: S . n = s * ((canFS (the_Vertices_of G)) ")
then dom (canFS (the_Vertices_of G)) c= Seg n by A6, FINSEQ_1:5;
then (canFS (the_Vertices_of G)) | (Seg n) = canFS (the_Vertices_of G) by RELAT_1:68;
hence S . n = s * ((canFS (the_Vertices_of G)) ") by A4; :: thesis: verum

end;

A7: now :: thesis: for i being Nat holds S . i is PartFunc of (the_Vertices_of G),NAT

let i be Nat; :: thesis: S . i is PartFunc of (the_Vertices_of G),NAT
set Si = s * (((canFS (the_Vertices_of G)) | (Seg i)) ");
A8: rng (s * (((canFS (the_Vertices_of G)) | (Seg i)) ")) c= NAT ;
(canFS (the_Vertices_of G)) | (Seg i) is one-to-one by FUNCT_1:52;
then A9: ((canFS (the_Vertices_of G)) | (Seg i)) ~ = ((canFS (the_Vertices_of G)) | (Seg i)) " by FUNCT_1:def 5;

now :: thesis: for x being object st x in dom (s * (((canFS (the_Vertices_of G)) | (Seg i)) ")) holds
x in the_Vertices_of G

let x be object ; :: thesis: ( x in dom (s * (((canFS (the_Vertices_of G)) | (Seg i)) ")) implies x in the_Vertices_of G )
assume x in dom (s * (((canFS (the_Vertices_of G)) | (Seg i)) ")) ; :: thesis: x in the_Vertices_of G
then x in dom (((canFS (the_Vertices_of G)) | (Seg i)) ") by FUNCT_1:11;
then x in rng ((canFS (the_Vertices_of G)) | (Seg i)) by A9, RELAT_1:20;
hence x in the_Vertices_of G ; :: thesis: verum

end;

then A10: dom (s * (((canFS (the_Vertices_of G)) | (Seg i)) ")) c= the_Vertices_of G ;
S . i = s * (((canFS (the_Vertices_of G)) | (Seg i)) ") by A4;
hence S . i is PartFunc of (the_Vertices_of G),NAT by A10, A8, RELSET_1:4; :: thesis: verum

end;

A11: dom s = NAT by FUNCT_2:def 1;
A12: for n being Nat st n <= len (canFS (the_Vertices_of G)) holds
card (S . n) = n

proof

let n be Nat; :: thesis: ( n <= len (canFS (the_Vertices_of G)) implies card (S . n) = n )
assume n <= len (canFS (the_Vertices_of G)) ; :: thesis: card (S . n) = n
then A13: Seg n c= Seg (len (canFS (the_Vertices_of G))) by FINSEQ_1:5;
A14: (canFS (the_Vertices_of G)) | (Seg n) is one-to-one by FUNCT_1:52;
A15: S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) ") by A4;
A16: card (Seg n) = n by FINSEQ_1:57;
dom (canFS (the_Vertices_of G)) = Seg (len (canFS (the_Vertices_of G))) by FINSEQ_1:def 3;
then A17: dom ((canFS (the_Vertices_of G)) | (Seg n)) = Seg n by A13, RELAT_1:62;
then rng (((canFS (the_Vertices_of G)) | (Seg n)) ") = Seg n by A14, FUNCT_1:33;
then dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) ")) = dom (((canFS (the_Vertices_of G)) | (Seg n)) ") by A11, RELAT_1:27
.= rng ((canFS (the_Vertices_of G)) | (Seg n)) by A14, FUNCT_1:33 ;
then card (dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) "))) = n by A14, A17, A16, CARD_1:70;
hence card (S . n) = n by A15, CARD_1:62; :: thesis: verum

end;

reconsider S = S as preVNumberingSeq of G by A7, Def7;
A18: len (canFS (the_Vertices_of G)) = card (the_Vertices_of G) by FINSEQ_1:93;
A19: S is iterative

proof

A20: for k, n being Nat st k < n & S . k = S . n holds
S . (k + 1) = S . (n + 1)

proof

let k, n be Nat; :: thesis: ( k < n & S . k = S . n implies S . (k + 1) = S . (n + 1) )
assume that
A21: k < n and
A22: S . k = S . n ; :: thesis: S . (k + 1) = S . (n + 1)

per cases ( n < card (the_Vertices_of G) or card (the_Vertices_of G) <= n ) ;

suppose A23: n < card (the_Vertices_of G) ; :: thesis: S . (k + 1) = S . (n + 1)

then card (S . n) = n by A18, A12;
hence S . (k + 1) = S . (n + 1) by A18, A12, A21, A22, A23, XXREAL_0:2; :: thesis: verum

end;

suppose A24: card (the_Vertices_of G) <= n ; :: thesis: S . (k + 1) = S . (n + 1)

per cases ( k < card (the_Vertices_of G) or k >= card (the_Vertices_of G) ) ;

suppose A25: k < card (the_Vertices_of G) ; :: thesis: S . (k + 1) = S . (n + 1)

A26: rng ((canFS (the_Vertices_of G)) ") c= dom s

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ((canFS (the_Vertices_of G)) ") or x in dom s )
assume x in rng ((canFS (the_Vertices_of G)) ") ; :: thesis: x in dom s
then x in rng ((canFS (the_Vertices_of G)) ~) by FUNCT_1:def 5;
then x in dom (canFS (the_Vertices_of G)) by RELAT_1:20;
then x in NAT ;
hence x in dom s by FUNCT_2:def 1; :: thesis: verum

end;

A27: S . n = ((canFS (the_Vertices_of G)) ") * s by A18, A5, A24;
card (S . n) = card (dom (S . n)) by CARD_1:62
.= card (dom ((canFS (the_Vertices_of G)) ")) by A27, A26, RELAT_1:27
.= card (rng (canFS (the_Vertices_of G))) by FUNCT_1:33
.= card (dom (canFS (the_Vertices_of G))) by CARD_1:70
.= len (canFS (the_Vertices_of G)) by CARD_1:62 ;
hence S . (k + 1) = S . (n + 1) by A18, A12, A22, A25; :: thesis: verum

end;

suppose A28: k >= card (the_Vertices_of G) ; :: thesis: S . (k + 1) = S . (n + 1)

A29: n + 1 >= card (the_Vertices_of G) by A24, NAT_1:13;
k + 1 >= card (the_Vertices_of G) by A28, NAT_1:13;
hence S . (k + 1) = s * ((canFS (the_Vertices_of G)) ") by A18, A5
.= S . (n + 1) by A18, A5, A29 ;
:: thesis: verum

end;

end;

end;

end;

end;

let k, n be Nat; :: according to LEXBFS:def 6 :: thesis: ( S . k = S . n implies S . (k + 1) = S . (n + 1) )
assume A30: S . k = S . n ; :: thesis: S . (k + 1) = S . (n + 1)

per cases ( k < n or k > n or k = n ) by XXREAL_0:1;

suppose k < n ; :: thesis: S . (k + 1) = S . (n + 1)

hence S . (k + 1) = S . (n + 1) by A20, A30; :: thesis: verum

end;

suppose k > n ; :: thesis: S . (k + 1) = S . (n + 1)

hence S . (k + 1) = S . (n + 1) by A20, A30; :: thesis: verum

end;

suppose k = n ; :: thesis: S . (k + 1) = S . (n + 1)

hence S . (k + 1) = S . (n + 1) ; :: thesis: verum

end;

end;

end;

reconsider N = card (the_Vertices_of G) as Element of NAT ;
A31: N <= N + 1 by NAT_1:11;
A32: N >= len (canFS (the_Vertices_of G)) by FINSEQ_1:93;
then A33: S . N = s * ((canFS (the_Vertices_of G)) ") by A5
.= S . (N + 1) by A5, A32, A31, XXREAL_0:2 ;
then A34: S is halting ;
A35: for n being Nat st S . n = S . (n + 1) holds
N <= n

proof

let n be Nat; :: thesis: ( S . n = S . (n + 1) implies N <= n )
assume that
A36: S . n = S . (n + 1) and
A37: N > n ; :: thesis: contradiction
A38: n + 1 <= N by A37, NAT_1:13;
n = card (S . (n + 1)) by A18, A12, A36, A37
.= n + 1 by A18, A12, A38 ;
hence contradiction ; :: thesis: verum

end;

then A39: S .Lifespan() = G .order() by A33, A34, GLIB_000:def 56;

A40: now :: thesis: for n being Nat st n < S .Lifespan() holds
ex w being Vertex of G st
( not w in dom (S . n) & S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) )

let n be Nat; :: thesis: ( n < S .Lifespan() implies ex w being Vertex of G st
( not w in dom (S . n) & S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) ) )
assume A41: n < S .Lifespan() ; :: thesis: ex w being Vertex of G st
( not w in dom (S . n) & S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) )
n < N by A33, A34, A35, A41, GLIB_000:def 56;
then A42: n + 1 <= N by NAT_1:13;
set w = (canFS (the_Vertices_of G)) . (n + 1);
A43: 0 + 1 <= n + 1 by NAT_1:13;
n + 1 <= len (canFS (the_Vertices_of G)) by A42, FINSEQ_1:93;
then A44: n + 1 in dom (canFS (the_Vertices_of G)) by A43, FINSEQ_3:25;
then (canFS (the_Vertices_of G)) . (n + 1) in rng (canFS (the_Vertices_of G)) by FUNCT_1:3;
then reconsider w = (canFS (the_Vertices_of G)) . (n + 1) as Vertex of G ;
take w = w; :: thesis: ( not w in dom (S . n) & S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) )
A45: (canFS (the_Vertices_of G)) | (Seg n) is one-to-one by FUNCT_1:52;

hereby :: thesis: S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n))

assume w in dom (S . n) ; :: thesis: contradiction
then w in dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) ")) by A4;
then w in dom (((canFS (the_Vertices_of G)) | (Seg n)) ") by FUNCT_1:11;
then w in rng ((canFS (the_Vertices_of G)) | (Seg n)) by A45, FUNCT_1:33;
then consider x being object such that
A46: x in dom ((canFS (the_Vertices_of G)) | (Seg n)) and
A47: w = ((canFS (the_Vertices_of G)) | (Seg n)) . x by FUNCT_1:def 3;
A48: w = (canFS (the_Vertices_of G)) . x by A46, A47, FUNCT_1:47;
A49: x in Seg n by A46, RELAT_1:57;
A50: x in dom (canFS (the_Vertices_of G)) by A46, RELAT_1:57;
reconsider x = x as Nat by A46;
x <= n by A49, FINSEQ_1:1;
then x <> n + 1 by NAT_1:13;
hence contradiction by A44, A48, A50, FUNCT_1:def 4; :: thesis: verum

end;

A51: (canFS (the_Vertices_of G)) | (Seg (n + 1)) is one-to-one by FUNCT_1:52;
n <= n + 1 by NAT_1:11;
then A52: Seg n c= Seg (n + 1) by FINSEQ_1:5;

now :: thesis: ( dom (S . (n + 1)) = dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) & ( for x being object st x in dom (S . (n + 1)) holds
(S . (n + 1)) . x = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . x ) )

now :: thesis: for x being object holds
( ( x in dom (S . (n + 1)) implies x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) ) & ( x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) implies x in dom (S . (n + 1)) ) )

let x be object ; :: thesis: ( ( x in dom (S . (n + 1)) implies x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) ) & ( x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) implies b₁ in dom (S . (n + 1)) ) )

hereby :: thesis: ( x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) implies b₁ in dom (S . (n + 1)) )

assume x in dom (S . (n + 1)) ; :: thesis: x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n)))
then x in dom (s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ")) by A4;
then x in dom (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") by FUNCT_1:11;
then x in rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by A51, FUNCT_1:33;
then consider a being object such that
A53: a in dom ((canFS (the_Vertices_of G)) | (Seg (n + 1))) and
A54: x = ((canFS (the_Vertices_of G)) | (Seg (n + 1))) . a by FUNCT_1:def 3;
A55: a in Seg (n + 1) by A53, RELAT_1:57;
A56: dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) = (dom (S . n)) \/ (dom (w .--> ((S .Lifespan()) -' n))) by FUNCT_4:def 1;
reconsider a = a as Nat by A53;
A57: a in dom (canFS (the_Vertices_of G)) by A53, RELAT_1:57;
A58: a <= n + 1 by A55, FINSEQ_1:1;
A59: 1 <= a by A55, FINSEQ_1:1;

per cases ( a <= n or a = n + 1 ) by A58, NAT_1:8;

suppose a <= n ; :: thesis: x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n)))

then A60: a in Seg n by A59, FINSEQ_1:1;
then A61: a in dom ((canFS (the_Vertices_of G)) | (Seg n)) by A57, RELAT_1:57;
A62: ((canFS (the_Vertices_of G)) | (Seg n)) . a = (canFS (the_Vertices_of G)) . a by A60, FUNCT_1:49
.= x by A54, A55, FUNCT_1:49 ;
then x in rng ((canFS (the_Vertices_of G)) | (Seg n)) by A61, FUNCT_1:3;
then A63: x in dom (((canFS (the_Vertices_of G)) | (Seg n)) ") by A45, FUNCT_1:33;
(((canFS (the_Vertices_of G)) | (Seg n)) ") . x = a by A45, A61, A62, FUNCT_1:32;
then (((canFS (the_Vertices_of G)) | (Seg n)) ") . x in dom s by A11, ORDINAL1:def 12;
then x in dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) ")) by A63, FUNCT_1:11;
then x in dom (S . n) by A4;
hence x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) by A56, XBOOLE_0:def 3; :: thesis: verum

end;

suppose a = n + 1 ; :: thesis: x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n)))

then x = w by A53, A54, FUNCT_1:47;
then x in dom (w .--> ((S .Lifespan()) -' n)) by FUNCOP_1:74;
hence x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) by A56, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

assume x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) ; :: thesis: b₁ in dom (S . (n + 1))
then A64: x in (dom (S . n)) \/ (dom (w .--> ((S .Lifespan()) -' n))) by FUNCT_4:def 1;

per cases ( x in dom (S . n) or x in dom (w .--> ((S .Lifespan()) -' n)) ) by A64, XBOOLE_0:def 3;

suppose A65: x in dom (S . n) ; :: thesis: b₁ in dom (S . (n + 1))

(canFS (the_Vertices_of G)) | (Seg n) c= (canFS (the_Vertices_of G)) | (Seg (n + 1)) by A52, RELAT_1:75;
then A66: rng ((canFS (the_Vertices_of G)) | (Seg n)) c= rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by RELAT_1:11;
A67: x in dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) ")) by A4, A65;
then A68: x in dom (((canFS (the_Vertices_of G)) | (Seg n)) ") by FUNCT_1:11;
then x in rng ((canFS (the_Vertices_of G)) | (Seg n)) by A45, FUNCT_1:33;
then x in rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by A66;
then A69: x in dom (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") by A51, FUNCT_1:33;
A70: (((canFS (the_Vertices_of G)) | (Seg n)) ") . x in dom s by A67, FUNCT_1:11;
(((canFS (the_Vertices_of G)) | (Seg n)) ") . x = (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") . x by A52, A68, Lm2;
then x in dom (s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ")) by A70, A69, FUNCT_1:11;
hence x in dom (S . (n + 1)) by A4; :: thesis: verum

end;

suppose A71: x in dom (w .--> ((S .Lifespan()) -' n)) ; :: thesis: b₁ in dom (S . (n + 1))

A72: rng (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") = dom ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by A51, FUNCT_1:33;
x = w by A71, FUNCOP_1:75;
then x in rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by A44, FINSEQ_1:4, FUNCT_1:50;
then A73: x in dom (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") by A51, FUNCT_1:33;
then (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") . x in rng (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") by FUNCT_1:3;
then x in dom (s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ")) by A11, A73, A72, FUNCT_1:11;
hence x in dom (S . (n + 1)) by A4; :: thesis: verum

end;

end;

end;

hence A74: dom (S . (n + 1)) = dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) by TARSKI:2; :: thesis: for x being object st x in dom (S . (n + 1)) holds
(S . (n + 1)) . b₂ = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . b₂
let x be object ; :: thesis: ( x in dom (S . (n + 1)) implies (S . (n + 1)) . b₁ = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . b₁ )
assume A75: x in dom (S . (n + 1)) ; :: thesis: (S . (n + 1)) . b₁ = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . b₁
A76: x in (dom (S . n)) \/ (dom (w .--> ((S .Lifespan()) -' n))) by A74, A75, FUNCT_4:def 1;
A77: S . (n + 1) = s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") by A4;
A78: S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) ") by A4;

per cases ( x in dom (S . n) or x in dom (w .--> ((S .Lifespan()) -' n)) ) by A76, XBOOLE_0:def 3;

suppose A79: x in dom (S . n) ; :: thesis: (S . (n + 1)) . b₁ = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . b₁

then A80: x in dom (((canFS (the_Vertices_of G)) | (Seg n)) ") by A78, FUNCT_1:11;
then x in rng ((canFS (the_Vertices_of G)) | (Seg n)) by A45, FUNCT_1:33;
then consider m being object such that
A81: m in dom ((canFS (the_Vertices_of G)) | (Seg n)) and
A82: ((canFS (the_Vertices_of G)) | (Seg n)) . m = x by FUNCT_1:def 3;
A83: m in Seg n by A81, RELAT_1:57;
reconsider m = m as Nat by A81;
A84: m in dom (canFS (the_Vertices_of G)) by A81, RELAT_1:57;
m <= n by A83, FINSEQ_1:1;
then A85: m < n + 1 by NAT_1:13;
(canFS (the_Vertices_of G)) . m = x by A81, A82, FUNCT_1:47;
then A86: x <> w by A44, A84, A85, FUNCT_1:def 4;
thus (S . (n + 1)) . x = s . ((((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") . x) by A75, A77, FUNCT_1:12
.= s . ((((canFS (the_Vertices_of G)) | (Seg n)) ") . x) by A52, A80, Lm2
.= (S . n) . x by A78, A79, FUNCT_1:12
.= ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . x by A86, FUNCT_4:83 ; :: thesis: verum

end;

suppose A87: x in dom (w .--> ((S .Lifespan()) -' n)) ; :: thesis: (S . (n + 1)) . b₁ = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . b₁

n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A88: n + 1 in dom ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by A44, RELAT_1:57;
then A89: ((canFS (the_Vertices_of G)) | (Seg (n + 1))) . (n + 1) = w by FUNCT_1:47;
A90: x = w by A87, FUNCOP_1:75;
then x in rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by A44, FINSEQ_1:4, FUNCT_1:50;
then A91: x in dom (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") by A51, FUNCT_1:33;
A92: ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . x = (w .--> ((S .Lifespan()) -' n)) . x by A87, FUNCT_4:13
.= (S .Lifespan()) -' n by A90, FUNCOP_1:72 ;
(S . (n + 1)) . x = (s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) ")) . x by A4
.= s . ((((canFS (the_Vertices_of G)) | (Seg (n + 1))) ") . x) by A91, FUNCT_1:13
.= s . (n + 1) by A51, A90, A88, A89, FUNCT_1:32
.= (N -' (n + 1)) + 1 by A1
.= (N - (n + 1)) + 1 by A42, XREAL_1:233
.= N - n
.= (S .Lifespan()) -' n by A39, A41, XREAL_1:233 ;
hence (S . (n + 1)) . x = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . x by A92; :: thesis: verum

end;

end;

end;

hence S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n)) by FUNCT_1:2; :: thesis: verum

end;

take S ; :: thesis: S is vertex-numbering
card (S . 0) = 0 by A12;
then S . 0 = {} ;
hence S is vertex-numbering by A19, A34, A39, A40; :: thesis: verum