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 CSN = GS . n;
set VLN = GS . n;
set CN1 = GS . (n + 1);
set VN1 = GS . (n + 1);
set w = GS .PickedAt n;
A2: GS . (n + 1) = (GS . n) +* ((GS .PickedAt n) .--> ((GS .Lifespan() ) -' n)) by A1, Def27;
set f = (GS .PickedAt n) .--> ((GS .Lifespan() ) -' n);
( dom ((GS .PickedAt n) .--> ((GS .Lifespan() ) -' n)) = {(GS .PickedAt n)} & rng ((GS .PickedAt n) .--> ((GS .Lifespan() ) -' n)) = {((GS .Lifespan() ) -' n)} ) by FUNCOP_1:14, FUNCOP_1:19;
then A3: GS .PickedAt n in dom ((GS .PickedAt n) .--> ((GS .Lifespan() ) -' n)) by TARSKI:def 1;
((GS .PickedAt n) .--> ((GS .Lifespan() ) -' n)) . (GS .PickedAt n) = (GS .Lifespan() ) -' n by FUNCOP_1:87;
hence (GS . (n + 1)) . (GS .PickedAt n) = (GS .Lifespan() ) -' n by A2, A3, FUNCT_4:14; :: thesis: verum