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

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

end;

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