let G be finite _Graph; :: thesis: for n being Nat st n < G .order() holds
((MCS:CSeq G) ``1) .PickedAt n = MCS:PickUnnumbered ((MCS:CSeq G) . n)
let n be Nat; :: thesis: ( n < G .order() implies ((MCS:CSeq G) ``1) .PickedAt n = MCS:PickUnnumbered ((MCS:CSeq G) . n) )
assume A1: n < G .order() ; :: thesis: ((MCS:CSeq G) ``1) .PickedAt n = MCS:PickUnnumbered ((MCS:CSeq G) . n)
set GS = MCS:CSeq G;
set CSN = (MCS:CSeq G) . n;
set CS1 = (MCS:CSeq G) . (n + 1);
set VLN = ((MCS:CSeq G) . n) `1 ;
set VL1 = ((MCS:CSeq G) . (n + 1)) `1 ;
A2: (MCS:CSeq G) .Lifespan() = G .order() by Th70;
set PU = MCS:PickUnnumbered ((MCS:CSeq G) . n);
set f2 = (MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> (((MCS:CSeq G) .Lifespan()) -' n);
A3: dom ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> (((MCS:CSeq G) .Lifespan()) -' n)) = {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by FUNCOP_1:13;
n = card (dom (((MCS:CSeq G) . n) `1)) by A1, Th65;
then ((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> (((MCS:CSeq G) .Lifespan()) -' n)) by A1, A2, Th64;
then A4: dom (((MCS:CSeq G) . (n + 1)) `1) = (dom (((MCS:CSeq G) . n) `1)) \/ {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by A3, FUNCT_4:def 1;
A5: ((MCS:CSeq G) ``1) .Lifespan() = (MCS:CSeq G) .Lifespan() by Th72;
set PA = ((MCS:CSeq G) ``1) .PickedAt n;
set f1 = (((MCS:CSeq G) ``1) .PickedAt n) .--> (((MCS:CSeq G) .Lifespan()) -' n);
A6: dom ((((MCS:CSeq G) ``1) .PickedAt n) .--> (((MCS:CSeq G) .Lifespan()) -' n)) = {(((MCS:CSeq G) ``1) .PickedAt n)} by FUNCOP_1:13;
A7: ((MCS:CSeq G) . n) `1 = ((MCS:CSeq G) ``1) . n by Def25;
((MCS:CSeq G) . (n + 1)) `1 = ((MCS:CSeq G) ``1) . (n + 1) by Def25;
then ((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1) +* ((((MCS:CSeq G) ``1) .PickedAt n) .--> (((MCS:CSeq G) .Lifespan()) -' n)) by A1, A2, A7, A5, Def10;
then A8: dom (((MCS:CSeq G) . (n + 1)) `1) = (dom (((MCS:CSeq G) . n) `1)) \/ {(((MCS:CSeq G) ``1) .PickedAt n)} by A6, FUNCT_4:def 1;
A9: not ((MCS:CSeq G) ``1) .PickedAt n in dom (((MCS:CSeq G) . n) `1) by A1, A2, A7, A5, Def10;

now

assume ((MCS:CSeq G) ``1) .PickedAt n <> MCS:PickUnnumbered ((MCS:CSeq G) . n) ; :: thesis: contradiction
then not ((MCS:CSeq G) ``1) .PickedAt n in {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by TARSKI:def 1;
then A10: not ((MCS:CSeq G) ``1) .PickedAt n in dom (((MCS:CSeq G) . (n + 1)) `1) by A9, A4, XBOOLE_0:def 3;
((MCS:CSeq G) ``1) .PickedAt n in {(((MCS:CSeq G) ``1) .PickedAt n)} by TARSKI:def 1;
hence contradiction by A8, A10, XBOOLE_0:def 3; :: thesis: verum

end;

hence ((MCS:CSeq G) ``1) .PickedAt n = MCS:PickUnnumbered ((MCS:CSeq G) . n) ; :: thesis: verum