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))} by FUNCOP_1:19;
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 Def16;
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)} by FUNCOP_1:19;
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 Def16;
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, Def10;
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, Def10;

now

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