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₁[ Nat] means S . $1 is one-to-one ;
A1: S₁[ 0 ] by dVNumSeq;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
set CSK = S . k;
set VLK = S . k;
set CK1 = S . (k + 1);
set VL1 = S . (k + 1);
set GN = S .Lifespan() ;
set w = S .PickedAt k;

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

suppose k < S .Lifespan() ; :: thesis: S₁[k + 1]

then A4: S . (k + 1) = (S . k) +* ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) by Def27;
set wf = (S .PickedAt k) .--> ((S .Lifespan() ) -' k);
A5: ( dom ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) = {(S .PickedAt k)} & rng ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) = {((S .Lifespan() ) -' k)} ) by FUNCOP_1:14, FUNCOP_1:19;

now

assume A6: (S .Lifespan() ) -' k in rng (S . k) ; :: thesis: contradiction
rng (S . k) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' k)) by Th21;
hence contradiction by A6, Th5; :: thesis: verum

end;

then rng ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) misses rng (S . k) by A5, ZFMISC_1:56;
hence S₁[k + 1] by A3, A4, FUNCT_4:98; :: thesis: verum

end;

suppose A7: k >= S .Lifespan() ; :: thesis: S₁[k + 1]

k <= k + 1 by NAT_1:13;
hence S₁[k + 1] by A3, A7, Th17; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence S . n is one-to-one ; :: thesis: verum