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