let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G
for m, n being Nat st n < S .Lifespan() & n < m holds
( S .PickedAt n in dom (S . m) & (S . m) . (S .PickedAt n) = (S .Lifespan()) -' n )
let S be VNumberingSeq of G; :: thesis: for m, n being Nat st n < S .Lifespan() & n < m holds
( S .PickedAt n in dom (S . m) & (S . m) . (S .PickedAt n) = (S .Lifespan()) -' n )
let m, n be Nat; :: thesis: ( n < S .Lifespan() & n < m implies ( S .PickedAt n in dom (S . m) & (S . m) . (S .PickedAt n) = (S .Lifespan()) -' n ) )
assume that
A1: n < S .Lifespan() and
A2: n < m ; :: thesis: ( S .PickedAt n in dom (S . m) & (S . m) . (S .PickedAt n) = (S .Lifespan()) -' n )
set CN1 = S . (n + 1);
set VN1 = S . (n + 1);
set v = S .PickedAt n;
A3: (S . (n + 1)) . (S .PickedAt n) = (S .Lifespan()) -' n by A1, Th12;
set CSM = S . m;
set VLM = S . m;
n + 1 <= m by A2, NAT_1:13;
then S . (n + 1) c= S . m by Th17;
then A4: dom (S . (n + 1)) c= dom (S . m) by RELAT_1:11;
S .PickedAt n in dom (S . (n + 1)) by A1, Th11;
hence ( S .PickedAt n in dom (S . m) & (S . m) . (S .PickedAt n) = (S .Lifespan()) -' n ) by A3, A4, Th19; :: thesis: verum