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 PA = ((MCS:CSeq G) ``1 ) .PickedAt n;
set PU = MCS:PickUnnumbered ((MCS:CSeq G) . n);
set VLN = ((MCS:CSeq G) . n) `1 ;
set VL1 = ((MCS:CSeq G) . (n + 1)) `1 ;
A2: (MCS:CSeq G) .Lifespan() = G .order() by Th87;
A2a: ((MCS:CSeq G) . n) `1 = ((MCS:CSeq G) ``1 ) . n by d1stMCSLS;
A2b: ((MCS:CSeq G) . (n + 1)) `1 = ((MCS:CSeq G) ``1 ) . (n + 1) by d1stMCSLS;
((MCS:CSeq G) ``1 ) .Lifespan() = (MCS:CSeq G) .Lifespan() by mVNS0;
then A3: ( not ((MCS:CSeq G) ``1 ) .PickedAt n in dom (((MCS:CSeq G) . n) `1 ) & ((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1 ) +* ((((MCS:CSeq G) ``1 ) .PickedAt n) .--> (((MCS:CSeq G) .Lifespan() ) -' n)) ) by A2a, A2b, A2, A1, Def27;
n = card (dom (((MCS:CSeq G) . n) `1 )) by A1, Th82;
then A4: ((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, Th81;
set f1 = (((MCS:CSeq G) ``1 ) .PickedAt n) .--> (((MCS:CSeq G) .Lifespan() ) -' n);
set f2 = (MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> (((MCS:CSeq G) .Lifespan() ) -' n);
A5: ( dom ((((MCS:CSeq G) ``1 ) .PickedAt n) .--> (((MCS:CSeq G) .Lifespan() ) -' n)) = {(((MCS:CSeq G) ``1 ) .PickedAt n)} & rng ((((MCS:CSeq G) ``1 ) .PickedAt n) .--> (((MCS:CSeq G) .Lifespan() ) -' n)) = {(((MCS:CSeq G) .Lifespan() ) -' n)} ) by FUNCOP_1:14, FUNCOP_1:19;
A6: ( dom ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> (((MCS:CSeq G) .Lifespan() ) -' n)) = {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} & rng ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> (((MCS:CSeq G) .Lifespan() ) -' n)) = {(((MCS:CSeq G) .Lifespan() ) -' n)} ) by FUNCOP_1:14, FUNCOP_1:19;
A7: dom (((MCS:CSeq G) . (n + 1)) `1 ) = (dom (((MCS:CSeq G) . n) `1 )) \/ {(((MCS:CSeq G) ``1 ) .PickedAt n)} by A3, A5, FUNCT_4:def 1;
A8: dom (((MCS:CSeq G) . (n + 1)) `1 ) = (dom (((MCS:CSeq G) . n) `1 )) \/ {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by A4, A6, FUNCT_4:def 1;

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 A9: not ((MCS:CSeq G) ``1 ) .PickedAt n in dom (((MCS:CSeq G) . (n + 1)) `1 ) by A3, A8, XBOOLE_0:def 3;
((MCS:CSeq G) ``1 ) .PickedAt n in {(((MCS:CSeq G) ``1 ) .PickedAt n)} by TARSKI:def 1;
hence contradiction by A7, A9, XBOOLE_0:def 3; :: thesis: verum

end;

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