let G be _finite _Graph; :: thesis: for S being VNumberingSeq of G
for m, n being Nat
for v being set st v in dom (S . m) & (S . m) . v = n holds
S .PickedAt ((S .Lifespan()) -' n) = v
let S be VNumberingSeq of G; :: thesis: for m, n being Nat
for v being set st v in dom (S . m) & (S . m) . v = n holds
S .PickedAt ((S .Lifespan()) -' n) = v
let m, n be Nat; :: thesis: for v being set st v in dom (S . m) & (S . m) . v = n holds
S .PickedAt ((S .Lifespan()) -' n) = v
let v be set ; :: thesis: ( v in dom (S . m) & (S . m) . v = n implies S .PickedAt ((S .Lifespan()) -' n) = v )
set CSM = S . m;
set VLM = S . m;
set j = (S .Lifespan()) -' n;
set CJ1 = S . (((S .Lifespan()) -' n) + 1);
set VJ1 = S . (((S .Lifespan()) -' n) + 1);
assume that
A1: v in dom (S . m) and
A2: (S . m) . v = n ; :: thesis: S .PickedAt ((S .Lifespan()) -' n) = v
set w = S .PickedAt ((S .Lifespan()) -' n);
n <= S .Lifespan() by A2, Th15;
then A3: (S .Lifespan()) -' n = (S .Lifespan()) - n by XREAL_1:233;
A4: 0 < n by A1, A2, Th15;
then A5: (S .Lifespan()) -' n < S .Lifespan() by A3, XREAL_1:44;
then (S .Lifespan()) -' ((S .Lifespan()) -' n) = (S .Lifespan()) - ((S .Lifespan()) - n) by A3, XREAL_1:233;
then A6: (S . (((S .Lifespan()) -' n) + 1)) . (S .PickedAt ((S .Lifespan()) -' n)) = n by A4, A3, Th12, XREAL_1:44;
A7: S . m is one-to-one by Th18;
A8: S .PickedAt ((S .Lifespan()) -' n) in dom (S . (((S .Lifespan()) -' n) + 1)) by A5, Th11;

per cases ( m <= (S .Lifespan()) -' n or (S .Lifespan()) -' n < m ) ;

suppose A9: m <= (S .Lifespan()) -' n ; :: thesis: S .PickedAt ((S .Lifespan()) -' n) = v

then m + n <= ((S .Lifespan()) - n) + n by A3, XREAL_1:6;
then A10: (n + m) - m <= (S .Lifespan()) - m by XREAL_1:9;
A11: rng (S . m) = (Seg (S .Lifespan())) \ (Seg ((S .Lifespan()) -' m)) by Th14;
A12: n in rng (S . m) by A1, A2, FUNCT_1:def 3;
(S .Lifespan()) - m = (S .Lifespan()) -' m by A5, A9, XREAL_1:233, XXREAL_0:2;
hence S .PickedAt ((S .Lifespan()) -' n) = v by A10, A12, A11, Th3; :: thesis: verum

end;

suppose (S .Lifespan()) -' n < m ; :: thesis: S .PickedAt ((S .Lifespan()) -' n) = v

then ((S .Lifespan()) -' n) + 1 <= m by NAT_1:13;
then A13: S . (((S .Lifespan()) -' n) + 1) c= S . m by Th17;
then A14: dom (S . (((S .Lifespan()) -' n) + 1)) c= dom (S . m) by RELAT_1:11;
[(S .PickedAt ((S .Lifespan()) -' n)),n] in S . (((S .Lifespan()) -' n) + 1) by A8, A6, FUNCT_1:def 2;
then (S . m) . (S .PickedAt ((S .Lifespan()) -' n)) = n by A8, A13, A14, FUNCT_1:def 2;
hence S .PickedAt ((S .Lifespan()) -' n) = v by A1, A2, A8, A7, A14, FUNCT_1:def 4; :: thesis: verum

end;

end;