set N = card (the_Vertices_of G);

set vs = canFS (the_Vertices_of G);

deffunc H_{1}( 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_{1}(n)
from FUNCT_2:sch 4();

defpred S_{1}[ object , object ] means ex n being Nat st

( G = n & c_{2} = s * (((canFS (the_Vertices_of G)) | (Seg n)) ") );

A2: for n being object st n in NAT holds

ex j being object st S_{1}[n,j]

A3: for n being object st n in NAT holds

S_{1}[n,S . n]
from PBOOLE:sch 3(A2);

A4: for n being Nat holds S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) ")

S . n = s * ((canFS (the_Vertices_of G)) ")

A12: for n being Nat st n <= len (canFS (the_Vertices_of G)) holds

card (S . n) = n

A18: len (canFS (the_Vertices_of G)) = card (the_Vertices_of G) by FINSEQ_1:93;

A19: S is iterative

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

card (S . 0) = 0 by A12;

then S . 0 = {} ;

hence S is vertex-numbering by A19, A34, A39, A40; :: thesis: verum

set vs = canFS (the_Vertices_of G);

deffunc H

consider s being sequence of NAT such that

A1: for n being Element of NAT holds s . n = H

defpred S

( G = n & c

A2: for n being object st n in NAT holds

ex j being object st S

proof

consider S being ManySortedSet of NAT such that
let n be object ; :: thesis: ( n in NAT implies ex j being object st S_{1}[n,j] )

assume n in NAT ; :: thesis: ex j being object st S_{1}[n,j]

then reconsider n9 = n as Nat ;

take s * (((canFS (the_Vertices_of G)) | (Seg n9)) ") ; :: thesis: S_{1}[n,s * (((canFS (the_Vertices_of G)) | (Seg n9)) ")]

thus S_{1}[n,s * (((canFS (the_Vertices_of G)) | (Seg n9)) ")]
; :: thesis: verum

end;assume n in NAT ; :: thesis: ex j being object st S

then reconsider n9 = n as Nat ;

take s * (((canFS (the_Vertices_of G)) | (Seg n9)) ") ; :: thesis: S

thus S

A3: for n being object st n in NAT holds

S

A4: for n being Nat holds S . n = s * (((canFS (the_Vertices_of G)) | (Seg n)) ")

proof

A5:
for n being Nat st n >= len (canFS (the_Vertices_of G)) holds
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;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

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;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

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

A11:
dom s = NAT
by FUNCT_2:def 1;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;

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;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

then A10:
dom (s * (((canFS (the_Vertices_of G)) | (Seg i)) ")) c= the_Vertices_of G
;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;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

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

A12: for n being Nat st n <= len (canFS (the_Vertices_of G)) holds

card (S . n) = n

proof

reconsider S = S as preVNumberingSeq of G by A7, Def7;
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;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

A18: len (canFS (the_Vertices_of G)) = card (the_Vertices_of G) by FINSEQ_1:93;

A19: S is iterative

proof

reconsider N = card (the_Vertices_of G) as Element of NAT ;
A20:
for k, n being Nat st k < n & S . k = S . n holds

S . (k + 1) = S . (n + 1)

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

end;S . (k + 1) = S . (n + 1)

proof

let k, n be Nat; :: according to LEXBFS:def 6 :: thesis: ( S . k = S . n implies S . (k + 1) = S . (n + 1) )
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)

end;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 )
;

end;

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;hence S . (k + 1) = S . (n + 1) by A18, A12, A21, A22, A23, XXREAL_0:2; :: thesis: verum

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

end;

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

end;

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

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;proof

A27:
S . n = ((canFS (the_Vertices_of G)) ") * s
by A18, A5, A24;
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;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

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

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;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

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

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

then A39:
S .Lifespan() = G .order()
by A33, A34, GLIB_000:def 56;
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;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

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)) )

take
S
; :: thesis: S is vertex-numbering 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;

n <= n + 1 by NAT_1:11;

then A52: Seg n c= Seg (n + 1) by FINSEQ_1:5;

end;( 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))

A51:
(canFS (the_Vertices_of G)) | (Seg (n + 1)) is one-to-one
by FUNCT_1:52;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;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

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 ) )

(S . (n + 1)) . b_{2} = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . b_{2}

let x be object ; :: thesis: ( x in dom (S . (n + 1)) implies (S . (n + 1)) . b_{1} = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . b_{1} )

assume A75: x in dom (S . (n + 1)) ; :: thesis: (S . (n + 1)) . b_{1} = ((S . n) +* (w .--> ((S .Lifespan()) -' n))) . b_{1}

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;

end;

hence
S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan()) -' n))
by FUNCT_1:2; :: thesis: verum(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)) ) )

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 ( ( 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_{1} in dom (S . (n + 1)) ) )

_{1} in dom (S . (n + 1))

then A64: x in (dom (S . n)) \/ (dom (w .--> ((S .Lifespan()) -' n))) by FUNCT_4:def 1;

end;hereby :: thesis: ( x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n))) implies b_{1} in dom (S . (n + 1)) )

assume
x in dom ((S . n) +* (w .--> ((S .Lifespan()) -' n)))
; :: thesis: bassume
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;

end;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;

end;

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;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

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;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

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;

end;

suppose A65:
x in dom (S . n)
; :: thesis: b_{1} 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;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

suppose A71:
x in dom (w .--> ((S .Lifespan()) -' n))
; :: thesis: b_{1} 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;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

(S . (n + 1)) . b

let x be object ; :: thesis: ( x in dom (S . (n + 1)) implies (S . (n + 1)) . b

assume A75: x in dom (S . (n + 1)) ; :: thesis: (S . (n + 1)) . 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;

end;

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

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;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

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

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;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

card (S . 0) = 0 by A12;

then S . 0 = {} ;

hence S is vertex-numbering by A19, A34, A39, A40; :: thesis: verum