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 A1: ( v in dom (S . m) & (S . m) . v = n ) ; :: thesis: S .PickedAt ((S .Lifespan() ) -' n) = v
then A2: ( 1 <= n & n <= S .Lifespan() ) by Th22;
A3: 0 < n by A1, Th22;
A4: (S .Lifespan() ) -' n = (S .Lifespan() ) - n by A2, XREAL_1:235;
then A5: (S .Lifespan() ) -' n < S .Lifespan() by A3, XREAL_1:46;
set w = S .PickedAt ((S .Lifespan() ) -' n);
A6: S .PickedAt ((S .Lifespan() ) -' n) in dom (S . (((S .Lifespan() ) -' n) + 1)) by A5, Th18;
(S .Lifespan() ) -' ((S .Lifespan() ) -' n) = (S .Lifespan() ) - ((S .Lifespan() ) - n) by A4, A5, XREAL_1:235;
then A7: (S . (((S .Lifespan() ) -' n) + 1)) . (S .PickedAt ((S .Lifespan() ) -' n)) = n by A3, A4, Th19, XREAL_1:46;
A8: S . m is one-to-one by Th25;

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 A4, XREAL_1:8;
then A10: (n + m) - m <= (S .Lifespan() ) - m by XREAL_1:11;
A11: (S .Lifespan() ) - m = (S .Lifespan() ) -' m by A5, A9, XREAL_1:235, XXREAL_0:2;
A12: n in rng (S . m) by A1, FUNCT_1:def 5;
rng (S . m) = (Seg (S .Lifespan() )) \ (Seg ((S .Lifespan() ) -' m)) by Th21;
hence S .PickedAt ((S .Lifespan() ) -' n) = v by A10, A11, A12, Th5; :: 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 Th24;
then A14: dom (S . (((S .Lifespan() ) -' n) + 1)) c= dom (S . m) by RELAT_1:25;
[(S .PickedAt ((S .Lifespan() ) -' n)),n] in S . (((S .Lifespan() ) -' n) + 1) by A6, A7, FUNCT_1:def 4;
then (S . m) . (S .PickedAt ((S .Lifespan() ) -' n)) = n by A6, A13, A14, FUNCT_1:def 4;
hence S .PickedAt ((S .Lifespan() ) -' n) = v by A1, A6, A8, A14, FUNCT_1:def 8; :: thesis: verum

end;

end;