let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G
for n being Nat st n < S .Lifespan() holds
(S . (n + 1)) . (S .PickedAt n) = (S .Lifespan()) -' n
let GS be VNumberingSeq of G; :: thesis: for n being Nat st n < GS .Lifespan() holds
(GS . (n + 1)) . (GS .PickedAt n) = (GS .Lifespan()) -' n
let n be Nat; :: thesis: ( n < GS .Lifespan() implies (GS . (n + 1)) . (GS .PickedAt n) = (GS .Lifespan()) -' n )
assume A1: n < GS .Lifespan() ; :: thesis: (GS . (n + 1)) . (GS .PickedAt n) = (GS .Lifespan()) -' n
set w = GS .PickedAt n;
set CN1 = GS . (n + 1);
set CSN = GS . n;
set VLN = GS . n;
set VN1 = GS . (n + 1);
set f = (GS .PickedAt n) .--> ((GS .Lifespan()) -' n);
A2: ((GS .PickedAt n) .--> ((GS .Lifespan()) -' n)) . (GS .PickedAt n) = (GS .Lifespan()) -' n by FUNCOP_1:72;
A3: GS .PickedAt n in dom ((GS .PickedAt n) .--> ((GS .Lifespan()) -' n)) by TARSKI:def 1;
GS . (n + 1) = (GS . n) +* ((GS .PickedAt n) .--> ((GS .Lifespan()) -' n)) by A1, Def9;
hence (GS . (n + 1)) . (GS .PickedAt n) = (GS .Lifespan()) -' n by A3, A2, FUNCT_4:13; :: thesis: verum