let G be finite _Graph; :: thesis: for S being VNumberingSeq of G
for n being Nat holds rng (S . n) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' n))
let S be VNumberingSeq of G; :: thesis: for n being Nat holds rng (S . n) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' n))
let n be Nat; :: thesis: rng (S . n) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' n))
set CSN = S . n;
set VLN = S . n;
set CSO = S . (S .Lifespan() );
set GN = S .Lifespan() ;
defpred S₁[ Nat] means ( $1 <= S .Lifespan() implies rng (S . $1) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' $1)) );
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
set CK1 = S . (k + 1);
set CSK = S . k;
set VLK = S . k;
set VK1 = S . (k + 1);

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

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

set w = S .PickedAt k;
set wf = (S .PickedAt k) .--> ((S .Lifespan() ) -' k);
A4: dom ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) = {(S .PickedAt k)} by FUNCOP_1:19;
A5: k < S .Lifespan() by A3, NAT_1:13;
then not S .PickedAt k in dom (S . k) by Def10;
then A6: dom ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) misses dom (S . k) by A4, ZFMISC_1:56;
A7: rng ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) = {((S .Lifespan() ) -' k)} by FUNCOP_1:14;
S . (k + 1) = (S . k) +* ((S .PickedAt k) .--> ((S .Lifespan() ) -' k)) by A5, Def10;
then rng (S . (k + 1)) = (rng (S . k)) \/ {((S .Lifespan() ) -' k)} by A7, A6, NECKLACE:7;
hence S₁[k + 1] by A2, A5, Th5; :: thesis: verum

end;

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

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

end;

end;

end;

A8: S₁[ 0 ]

proof

set CS0 = S . 0 ;
set VL0 = S . 0 ;
A9: (S .Lifespan() ) -' 0 = (S .Lifespan() ) - 0 by XREAL_1:235;
rng (S . 0 ) = {} by Def9, RELAT_1:60;
hence S₁[ 0 ] by A9, XBOOLE_1:37; :: thesis: verum

end;

A10: for k being Nat holds S₁[k] from NAT_1:sch 2(A8, A1);

per cases ( n <= S .Lifespan() or S .Lifespan() < n ) ;

suppose n <= S .Lifespan() ; :: thesis: rng (S . n) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' n))

hence rng (S . n) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' n)) by A10; :: thesis: verum

end;

suppose A11: S .Lifespan() < n ; :: thesis: rng (S . n) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' n))

then (S .Lifespan() ) - n < n - n by XREAL_1:11;
then (S .Lifespan() ) -' n = 0 by XREAL_0:def 2;
then A12: (S .Lifespan() ) -' (S .Lifespan() ) = (S .Lifespan() ) -' n by XREAL_1:234;
S . (S .Lifespan() ) = S . n by A11, Th9;
hence rng (S . n) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' n)) by A10, A12; :: thesis: verum

end;

end;