let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G
for n being Nat st n <= S .Lifespan() holds
card (dom (S . n)) = n
let S be VNumberingSeq of G; :: thesis: for n being Nat st n <= S .Lifespan() holds
card (dom (S . n)) = n
let n be Nat; :: thesis: ( n <= S .Lifespan() implies card (dom (S . n)) = n )
assume A1: n <= S .Lifespan() ; :: thesis: card (dom (S . n)) = n
defpred S₁[ Nat] means ( $1 <= S .Lifespan() implies card (dom (S . $1)) = $1 );
A2: for k being Nat st k < S .Lifespan() & card (dom (S . k)) = k holds
card (dom (S . (k + 1))) = k + 1

proof

let k be Nat; :: thesis: ( k < S .Lifespan() & card (dom (S . k)) = k implies card (dom (S . (k + 1))) = k + 1 )
assume that
A3: k < S .Lifespan() and
A4: card (dom (S . k)) = k ; :: thesis: card (dom (S . (k + 1))) = k + 1
set w = S .PickedAt k;
set CK1 = S . (k + 1);
set CSK = S . k;
set VLK = S . k;
set VK1 = S . (k + 1);
set wf = (S .PickedAt k) .--> ((S .Lifespan()) -' k);
A5: dom ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) = {(S .PickedAt k)} ;
S . (k + 1) = (S . k) +* ((S .PickedAt k) .--> ((S .Lifespan()) -' k)) by A3, Def9;
then A6: dom (S . (k + 1)) = (dom (S . k)) \/ {(S .PickedAt k)} by A5, FUNCT_4:def 1;
not S .PickedAt k in dom (S . k) by A3, Def9;
hence card (dom (S . (k + 1))) = k + 1 by A4, A6, CARD_2:41; :: thesis: verum

end;

A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

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

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

hence S₁[k + 1] by A2, A8; :: thesis: verum

end;

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

hence S₁[k + 1] by NAT_1:13; :: thesis: verum

end;

end;

end;

A9: S₁[ 0 ] by Def8, CARD_1:27, RELAT_1:38;
for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A7);
hence card (dom (S . n)) = n by A1; :: thesis: verum