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

proof

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

end;

consider S being ManySortedSet of NAT such that
B: for n being set st n in NAT holds
S₁[n,S . n] from PBOOLE:sch 3(P);
BB: 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 13;
then ex i' being Nat st
( n = i' & S . n = s * (((canFS (the_Vertices_of G)) | (Seg i')) " ) ) by B;
hence S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) " ) ; :: thesis: verum

end;

BE: len (canFS (the_Vertices_of G)) = card (the_Vertices_of G) by UPROOTS:5;
BC: 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 A2: n <= len (canFS (the_Vertices_of G)) ; :: thesis: card (S . n) = n
B2: S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) " ) by BB;
C2: Seg n c= Seg (len (canFS (the_Vertices_of G))) by A2, FINSEQ_1:7;
D2: (canFS (the_Vertices_of G)) | (Seg n) is one-to-one by FUNCT_1:84;
dom (canFS (the_Vertices_of G)) = Seg (len (canFS (the_Vertices_of G))) by FINSEQ_1:def 3;
then G2: dom ((canFS (the_Vertices_of G)) | (Seg n)) = Seg n by C2, RELAT_1:91;
then rng (((canFS (the_Vertices_of G)) | (Seg n)) " ) = Seg n by D2, FUNCT_1:55;
then F2: dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) " )) = dom (((canFS (the_Vertices_of G)) | (Seg n)) " ) by Ad, RELAT_1:46
.= rng ((canFS (the_Vertices_of G)) | (Seg n)) by D2, FUNCT_1:55 ;
card (Seg n) = n by FINSEQ_1:78;
then card (dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) " ))) = n by F2, G2, D2, TH2;
hence card (S . n) = n by B2, PRE_CIRC:21; :: thesis: verum

end;

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

proof

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

end;

now

let i be Nat; :: thesis: S . i is PartFunc of the_Vertices_of G, NAT
AB: S . i = s * (((canFS (the_Vertices_of G)) | (Seg i)) " ) by BB;
set Si = s * (((canFS (the_Vertices_of G)) | (Seg i)) " );
(canFS (the_Vertices_of G)) | (Seg i) is one-to-one by FUNCT_1:84;
then B2: ((canFS (the_Vertices_of G)) | (Seg i)) ~ = ((canFS (the_Vertices_of G)) | (Seg i)) " by FUNCT_1:def 9;

now

let x be set ; :: 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:21;
then x in rng ((canFS (the_Vertices_of G)) | (Seg i)) by B2, RELAT_1:37;
hence x in the_Vertices_of G ; :: thesis: verum

end;

then A1: dom (s * (((canFS (the_Vertices_of G)) | (Seg i)) " )) c= the_Vertices_of G by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in rng (s * (((canFS (the_Vertices_of G)) | (Seg i)) " )) implies x in NAT )
assume x in rng (s * (((canFS (the_Vertices_of G)) | (Seg i)) " )) ; :: thesis: x in NAT
then x in rng s by FUNCT_1:25;
hence x in NAT ; :: thesis: verum

end;

then rng (s * (((canFS (the_Vertices_of G)) | (Seg i)) " )) c= NAT by TARSKI:def 3;
hence S . i is PartFunc of the_Vertices_of G, NAT by AB, A1, RELSET_1:11; :: thesis: verum

end;

then reconsider S = S as preVNumberingSeq of G by dpVNumSeq;
take S ; :: thesis: S is vertex-numbering
card (S . 0 ) = 0 by BC;
then P: S . 0 = {} ;
Q: S is iterative

proof

A0: 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
A3: k < n and
B3: 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 S0: n < card (the_Vertices_of G) ; :: thesis: S . (k + 1) = S . (n + 1)

( card (S . n) = n & card (S . k) = k ) by S0, BC, BE, A3, XXREAL_0:2;
hence S . (k + 1) = S . (n + 1) by B3; :: thesis: verum

end;

suppose S0: 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 S1: k < card (the_Vertices_of G) ; :: thesis: S . (k + 1) = S . (n + 1)

B2: S . n = ((canFS (the_Vertices_of G)) " ) * s by S0, BD, BE;
C2: rng ((canFS (the_Vertices_of G)) " ) c= dom s

proof

let x be set ; :: 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 9;
then x in dom (canFS (the_Vertices_of G)) by RELAT_1:37;
then x in NAT ;
hence x in dom s by FUNCT_2:def 1; :: thesis: verum

end;

card (S . n) = card (dom (S . n)) by PRE_CIRC:21
.= card (dom ((canFS (the_Vertices_of G)) " )) by B2, C2, RELAT_1:46
.= card (rng (canFS (the_Vertices_of G))) by FUNCT_1:55
.= card (dom (canFS (the_Vertices_of G))) by TH2
.= len (canFS (the_Vertices_of G)) by PRE_CIRC:21 ;
hence S . (k + 1) = S . (n + 1) by BC, S1, B3, BE; :: thesis: verum

end;

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

A2: k + 1 >= card (the_Vertices_of G) by S1, NAT_1:13;
B2: n + 1 >= card (the_Vertices_of G) by S0, NAT_1:13;
thus S . (k + 1) = s * ((canFS (the_Vertices_of G)) " ) by A2, BD, BE
.= S . (n + 1) by B2, BD, BE ; :: 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 A1: 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 A0, A1; :: thesis: verum

end;

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

hence S . (k + 1) = S . (n + 1) by A0, A1; :: 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 ;
L1a: N >= len (canFS (the_Vertices_of G)) by UPROOTS:5;
L1c: N <= N + 1 by NAT_1:11;
L1: S . N = s * ((canFS (the_Vertices_of G)) " ) by L1a, BD
.= S . (N + 1) by L1a, L1c, XXREAL_0:2, BD ;
L0: S is halting by L1, GLIB_000:def 56;
L2: 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
A3: S . n = S . (n + 1) and
B3: N > n ; :: thesis: contradiction
C3: n + 1 <= N by B3, NAT_1:13;
n = card (S . (n + 1)) by A3, B3, BC, BE
.= n + 1 by C3, BC, BE ;
hence contradiction ; :: thesis: verum

end;

S: S .Lifespan() = G .order() by L0, L1, L2, GLIB_000:def 57;

now

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 A1: 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)) )
set w = (canFS (the_Vertices_of G)) . (n + 1);
( 0 <= n & n < N ) by A1, L0, L1, L2, GLIB_000:def 57;
then A1c: ( 0 + 1 <= n + 1 & n + 1 <= N ) by NAT_1:13;
( 1 <= n + 1 & n + 1 <= len (canFS (the_Vertices_of G)) ) by A1c, UPROOTS:5;
then A1a: n + 1 in dom (canFS (the_Vertices_of G)) by FINSEQ_3:27;
then (canFS (the_Vertices_of G)) . (n + 1) in rng (canFS (the_Vertices_of G)) by FUNCT_1:12;
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)) )
B1: (canFS (the_Vertices_of G)) | (Seg n) is one-to-one by FUNCT_1:84;
C1: (canFS (the_Vertices_of G)) | (Seg (n + 1)) is one-to-one by FUNCT_1:84;
n <= n + 1 by NAT_1:11;
then K5aa: Seg n c= Seg (n + 1) by FINSEQ_1:7;

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 BB;
then w in dom (((canFS (the_Vertices_of G)) | (Seg n)) " ) by FUNCT_1:21;
then w in rng ((canFS (the_Vertices_of G)) | (Seg n)) by B1, FUNCT_1:55;
then consider x being set such that
B2: x in dom ((canFS (the_Vertices_of G)) | (Seg n)) and
C2: w = ((canFS (the_Vertices_of G)) | (Seg n)) . x by FUNCT_1:def 5;
C2a: w = (canFS (the_Vertices_of G)) . x by B2, C2, FUNCT_1:70;
B2a: x in dom (canFS (the_Vertices_of G)) by B2, RELAT_1:86;
D2: x in Seg n by B2, RELAT_1:86;
reconsider x = x as Nat by B2;
x <= n by D2, FINSEQ_1:3;
then x <> n + 1 by NAT_1:13;
hence contradiction by A1a, C2a, B2a, FUNCT_1:def 8; :: thesis: verum

end;

now

now

let x be set ; :: 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 BB;
then x in dom (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) by FUNCT_1:21;
then x in rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by C1, FUNCT_1:55;
then consider a being set such that
A4: a in dom ((canFS (the_Vertices_of G)) | (Seg (n + 1))) and
B4: x = ((canFS (the_Vertices_of G)) | (Seg (n + 1))) . a by FUNCT_1:def 5;
C4: a in Seg (n + 1) by A4, RELAT_1:86;
reconsider a = a as Nat by A4;
D4: a in dom (canFS (the_Vertices_of G)) by A4, RELAT_1:86;
E4: dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) = (dom (S . n)) \/ (dom (w .--> ((S .Lifespan() ) -' n))) by FUNCT_4:def 1;
F4: a <= n + 1 by C4, FINSEQ_1:3;
C4a: 1 <= a by C4, FINSEQ_1:3;

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

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

then B5: a in Seg n by C4a, FINSEQ_1:3;
then A5: a in dom ((canFS (the_Vertices_of G)) | (Seg n)) by D4, RELAT_1:86;
C5: ((canFS (the_Vertices_of G)) | (Seg n)) . a = (canFS (the_Vertices_of G)) . a by B5, FUNCT_1:72
.= x by C4, B4, FUNCT_1:72 ;
then (((canFS (the_Vertices_of G)) | (Seg n)) " ) . x = a by B1, A5, FUNCT_1:54;
then D5: (((canFS (the_Vertices_of G)) | (Seg n)) " ) . x in dom s by Ad, ORDINAL1:def 13;
x in rng ((canFS (the_Vertices_of G)) | (Seg n)) by A5, C5, FUNCT_1:12;
then x in dom (((canFS (the_Vertices_of G)) | (Seg n)) " ) by B1, FUNCT_1:55;
then x in dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) " )) by D5, FUNCT_1:21;
then x in dom (S . n) by BB;
hence x in dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) by E4, 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 A4, B4, FUNCT_1:70;
then x in dom (w .--> ((S .Lifespan() ) -' n)) by FUNCOP_1:89;
hence x in dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) by E4, 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 A4: 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 A4, XBOOLE_0:def 3;

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

then A5: x in dom (s * (((canFS (the_Vertices_of G)) | (Seg n)) " )) by BB;
then B5: x in dom (((canFS (the_Vertices_of G)) | (Seg n)) " ) by FUNCT_1:21;
C5: (((canFS (the_Vertices_of G)) | (Seg n)) " ) . x in dom s by A5, FUNCT_1:21;
J5: (((canFS (the_Vertices_of G)) | (Seg n)) " ) . x = (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) . x by K5aa, B5, invrngrestr;
K5a: (canFS (the_Vertices_of G)) | (Seg n) c= (canFS (the_Vertices_of G)) | (Seg (n + 1)) by K5aa, RELAT_1:104;
K5: rng ((canFS (the_Vertices_of G)) | (Seg n)) c= rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by K5a, RELAT_1:25;
x in rng ((canFS (the_Vertices_of G)) | (Seg n)) by B5, B1, FUNCT_1:55;
then x in rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by K5;
then x in dom (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) by C1, FUNCT_1:55;
then x in dom (s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " )) by C5, J5, FUNCT_1:21;
hence x in dom (S . (n + 1)) by BB; :: thesis: verum

end;

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

then A5: x = w by FUNCOP_1:90;
x in rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by A1a, A5, FUNCT_1:73, FINSEQ_1:6;
then B5: x in dom (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) by C1, FUNCT_1:55;
C5: (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) . x in rng (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) by B5, FUNCT_1:12;
rng (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) = dom ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by C1, FUNCT_1:55;
then x in dom (s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " )) by Ad, C5, B5, FUNCT_1:21;
hence x in dom (S . (n + 1)) by BB; :: thesis: verum

end;

end;

end;

hence K3a: dom (S . (n + 1)) = dom ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) by TARSKI:2; :: thesis: for x being set st x in dom (S . (n + 1)) holds
(S . (n + 1)) . b₂ = ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . b₂
let x be set ; :: thesis: ( x in dom (S . (n + 1)) implies (S . (n + 1)) . b₁ = ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . b₁ )
assume K3: x in dom (S . (n + 1)) ; :: thesis: (S . (n + 1)) . b₁ = ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . b₁
L3: x in (dom (S . n)) \/ (dom (w .--> ((S .Lifespan() ) -' n))) by K3, K3a, FUNCT_4:def 1;
M3: S . (n + 1) = s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) by BB;
N3: S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) " ) by BB;

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

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

A5: ( x in dom (((canFS (the_Vertices_of G)) | (Seg n)) " ) & (((canFS (the_Vertices_of G)) | (Seg n)) " ) . x in dom s ) by N3, S4, FUNCT_1:21;
x in rng ((canFS (the_Vertices_of G)) | (Seg n)) by A5, B1, FUNCT_1:55;
then consider m being set such that
L5: m in dom ((canFS (the_Vertices_of G)) | (Seg n)) and
M5: ((canFS (the_Vertices_of G)) | (Seg n)) . m = x by FUNCT_1:def 5;
N5: m in Seg n by L5, RELAT_1:86;
reconsider m = m as Nat by L5;
O5: m <= n by N5, FINSEQ_1:3;
P5: (canFS (the_Vertices_of G)) . m = x by L5, M5, FUNCT_1:70;
R5: m in dom (canFS (the_Vertices_of G)) by L5, RELAT_1:86;
m < n + 1 by O5, NAT_1:13;
then S5: x <> w by A1a, P5, R5, FUNCT_1:def 8;
thus (S . (n + 1)) . x = s . ((((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) . x) by M3, K3, FUNCT_1:22
.= s . ((((canFS (the_Vertices_of G)) | (Seg n)) " ) . x) by A5, K5aa, invrngrestr
.= (S . n) . x by N3, S4, FUNCT_1:22
.= ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . x by S5, FUNCT_4:88 ; :: thesis: verum

end;

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

then A5: x = w by FUNCOP_1:90;
A5a: n + 1 in Seg (n + 1) by FINSEQ_1:6;
x in rng ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by FINSEQ_1:6, A1a, A5, FUNCT_1:73;
then B5: x in dom (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) by C1, FUNCT_1:55;
J5: n + 1 in dom ((canFS (the_Vertices_of G)) | (Seg (n + 1))) by A5a, A1a, RELAT_1:86;
K5a: ((canFS (the_Vertices_of G)) | (Seg (n + 1))) . (n + 1) = w by J5, FUNCT_1:70;
Z5: ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . x = (w .--> ((S .Lifespan() ) -' n)) . x by S4, FUNCT_4:14
.= (S .Lifespan() ) -' n by A5, FUNCOP_1:87 ;
(S . (n + 1)) . x = (s * (((canFS (the_Vertices_of G)) | (Seg (n + 1))) " )) . x by BB
.= s . ((((canFS (the_Vertices_of G)) | (Seg (n + 1))) " ) . x) by B5, FUNCT_1:23
.= s . (n + 1) by A5, J5, C1, K5a, FUNCT_1:54
.= (N -' (n + 1)) + 1 by A
.= (N - (n + 1)) + 1 by A1c, XREAL_1:235
.= N - n
.= (S .Lifespan() ) -' n by S, A1, XREAL_1:235 ;
hence (S . (n + 1)) . x = ((S . n) +* (w .--> ((S .Lifespan() ) -' n))) . x by Z5; :: thesis: verum

end;

end;

end;

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

end;

hence S is vertex-numbering by P, Q, L0, S, dVNumSeq; :: thesis: verum