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

suppose n >= S .Lifespan() ; :: thesis: ( ( n >= S .Lifespan() implies ex b₁ being set st b₁ = choose (the_Vertices_of G) ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan() ) -' n)) ) ) )

hence ( ( n >= S .Lifespan() implies ex b₁ being set st b₁ = choose (the_Vertices_of G) ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan() ) -' n)) ) ) ) ; :: thesis: verum

end;

suppose n < S .Lifespan() ; :: thesis: ( ( n >= S .Lifespan() implies ex b₁ being set st b₁ = choose (the_Vertices_of G) ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan() ) -' n)) ) ) )

then consider w being Vertex of G such that
A1: not w in dom (S . n) and
A2: S . (n + 1) = (S . n) +* (w .--> ((S .Lifespan() ) -' n)) by dVNumSeq;
thus ( ( n >= S .Lifespan() implies ex b₁ being set st b₁ = choose (the_Vertices_of G) ) & ( not n >= S .Lifespan() implies ex b₁ being set st
( not b₁ in dom (S . n) & S . (n + 1) = (S . n) +* (b₁ .--> ((S .Lifespan() ) -' n)) ) ) ) by A1, A2; :: thesis: verum

end;

end;