let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G

for n being Nat holds S . n is one-to-one

let S be VNumberingSeq of G; :: thesis: for n being Nat holds S . n is one-to-one

let n be Nat; :: thesis: S . n is one-to-one

defpred S_{1}[ Nat] means S . $1 is one-to-one ;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by Def8;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A8, A1);

hence S . n is one-to-one ; :: thesis: verum

for n being Nat holds S . n is one-to-one

let S be VNumberingSeq of G; :: thesis: for n being Nat holds S . n is one-to-one

let n be Nat; :: thesis: S . n is one-to-one

defpred S

A1: for k being Nat st S

S

proof

A8:
S
set GN = S .Lifespan() ;

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

set w = S .PickedAt k;

set CK1 = S . (k + 1);

set CSK = S . k;

set VLK = S . k;

set VL1 = S . (k + 1);

end;let k be Nat; :: thesis: ( S

assume A2: S

set w = S .PickedAt k;

set CK1 = S . (k + 1);

set CSK = S . k;

set VLK = S . k;

set VL1 = S . (k + 1);

per cases
( k < S .Lifespan() or k >= S .Lifespan() )
;

end;

suppose A3:
k < S .Lifespan()
; :: thesis: S_{1}[k + 1]

set wf = (S .PickedAt k) .--> ((S .Lifespan()) -' k);

then A6: rng ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) misses rng (S . k) by A4, ZFMISC_1:50;

S . (k + 1) = (S . k) +* ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) by A3, Def9;

hence S_{1}[k + 1]
by A2, A6, FUNCT_4:92; :: thesis: verum

end;A4: now :: thesis: not (S .Lifespan()) -' k in rng (S . k)

rng ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) = {((S .Lifespan()) -' k)}
by FUNCOP_1:8;assume A5:
(S .Lifespan()) -' k in rng (S . k)
; :: thesis: contradiction

rng (S . k) = (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' k)) by Th14;

hence contradiction by A5, Th3; :: thesis: verum

end;rng (S . k) = (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' k)) by Th14;

hence contradiction by A5, Th3; :: thesis: verum

then A6: rng ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) misses rng (S . k) by A4, ZFMISC_1:50;

S . (k + 1) = (S . k) +* ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) by A3, Def9;

hence S

for k being Nat holds S

hence S . n is one-to-one ; :: thesis: verum