let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G
for n being Nat st n < S .Lifespan() holds
( S .PickedAt n in dom (S . (n + 1)) & dom (S . (n + 1)) = (dom (S . n)) \/ {(S .PickedAt n)} )
let GS be VNumberingSeq of G; :: thesis: for n being Nat st n < GS .Lifespan() holds
( GS .PickedAt n in dom (GS . (n + 1)) & dom (GS . (n + 1)) = (dom (GS . n)) \/ {(GS .PickedAt n)} )
let n be Nat; :: thesis: ( n < GS .Lifespan() implies ( GS .PickedAt n in dom (GS . (n + 1)) & dom (GS . (n + 1)) = (dom (GS . n)) \/ {(GS .PickedAt n)} ) )
assume A1: n < GS .Lifespan() ; :: thesis: ( GS .PickedAt n in dom (GS . (n + 1)) & dom (GS . (n + 1)) = (dom (GS . n)) \/ {(GS .PickedAt n)} )
set f = (GS .PickedAt n) .--> ((GS .Lifespan()) -' n);
set CN1 = GS . (n + 1);
set CSN = GS . n;
set VLN = GS . n;
set VN1 = GS . (n + 1);
A2: dom ((GS .PickedAt n) .--> ((GS .Lifespan()) -' n)) = {(GS .PickedAt n)} ;
A3: GS .PickedAt n in {(GS .PickedAt n)} by TARSKI:def 1;
A4: GS . (n + 1) = (GS . n) +* ((GS .PickedAt n) .--> ((GS .Lifespan()) -' n)) by A1, Def9;
then dom (GS . (n + 1)) = (dom (GS . n)) \/ {(GS .PickedAt n)} by A2, FUNCT_4:def 1;
hence GS .PickedAt n in dom (GS . (n + 1)) by A3, XBOOLE_0:def 3; :: thesis: dom (GS . (n + 1)) = (dom (GS . n)) \/ {(GS .PickedAt n)}
thus dom (GS . (n + 1)) = (dom (GS . n)) \/ {(GS .PickedAt n)} by A4, A2, FUNCT_4:def 1; :: thesis: verum