let G be _finite _Graph; :: thesis: for n being Nat st n < G .order() holds
((LexBFS:CSeq G) ``1) .PickedAt n = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)
let n be Nat; :: thesis: ( n < G .order() implies ((LexBFS:CSeq G) ``1) .PickedAt n = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n) )
assume A1: n < G .order() ; :: thesis: ((LexBFS:CSeq G) ``1) .PickedAt n = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)
set CS = LexBFS:CSeq G;
set CSN = (LexBFS:CSeq G) . n;
set CS1 = (LexBFS:CSeq G) . (n + 1);
set VLN = ((LexBFS:CSeq G) . n) `1 ;
set VL1 = ((LexBFS:CSeq G) . (n + 1)) `1 ;
A2: (LexBFS:CSeq G) .Lifespan() = G .order() by Th37;
set PU = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n);
set f2 = (LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> (((LexBFS:CSeq G) .Lifespan()) -' n);
A3: dom ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> (((LexBFS:CSeq G) .Lifespan()) -' n)) = {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} ;
n = card (dom (((LexBFS:CSeq G) . n) `1)) by A1, Th32;
then ((LexBFS:CSeq G) . (n + 1)) `1 = (((LexBFS:CSeq G) . n) `1) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> (((LexBFS:CSeq G) .Lifespan()) -' n)) by A1, A2, Th31;
then A4: dom (((LexBFS:CSeq G) . (n + 1)) `1) = (dom (((LexBFS:CSeq G) . n) `1)) \/ {(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n))} by A3, FUNCT_4:def 1;
A5: ((LexBFS:CSeq G) . n) `1 = ((LexBFS:CSeq G) ``1) . n by Def15;
set PA = ((LexBFS:CSeq G) ``1) .PickedAt n;
set f1 = (((LexBFS:CSeq G) ``1) .PickedAt n) .--> (((LexBFS:CSeq G) .Lifespan()) -' n);
A6: dom ((((LexBFS:CSeq G) ``1) .PickedAt n) .--> (((LexBFS:CSeq G) .Lifespan()) -' n)) = {(((LexBFS:CSeq G) ``1) .PickedAt n)} ;
A7: (LexBFS:CSeq G) .Lifespan() = ((LexBFS:CSeq G) ``1) .Lifespan() by Th39;
((LexBFS:CSeq G) . (n + 1)) `1 = ((LexBFS:CSeq G) ``1) . (n + 1) by Def15;
then ((LexBFS:CSeq G) . (n + 1)) `1 = (((LexBFS:CSeq G) . n) `1) +* ((((LexBFS:CSeq G) ``1) .PickedAt n) .--> (((LexBFS:CSeq G) .Lifespan()) -' n)) by A1, A2, A7, A5, Def9;
then A8: dom (((LexBFS:CSeq G) . (n + 1)) `1) = (dom (((LexBFS:CSeq G) . n) `1)) \/ {(((LexBFS:CSeq G) ``1) .PickedAt n)} by A6, FUNCT_4:def 1;
A9: not ((LexBFS:CSeq G) ``1) .PickedAt n in dom (((LexBFS:CSeq G) . n) `1) by A1, A2, A7, A5, Def9;

now :: thesis: not ((LexBFS:CSeq G) ``1) .PickedAt n <> LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)

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

end;

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