let G be finite _Graph; :: thesis: for n being Nat st card (dom (((LexBFS:CSeq G) . n) `1)) < G .order() holds
((LexBFS:CSeq G) . (n + 1)) `1 = (((LexBFS:CSeq G) . n) `1) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((LexBFS:CSeq G) . n) `1)))))
let n be Nat; :: thesis: ( card (dom (((LexBFS:CSeq G) . n) `1)) < G .order() implies ((LexBFS:CSeq G) . (n + 1)) `1 = (((LexBFS:CSeq G) . n) `1) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((LexBFS:CSeq G) . n) `1))))) )
set CS = LexBFS:CSeq G;
assume A1: card (dom (((LexBFS:CSeq G) . n) `1)) < G .order() ; :: thesis: ((LexBFS:CSeq G) . (n + 1)) `1 = (((LexBFS:CSeq G) . n) `1) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((LexBFS:CSeq G) . n) `1)))))
set CN1 = (LexBFS:CSeq G) . (n + 1);
set CSN = (LexBFS:CSeq G) . n;
set VLN = ((LexBFS:CSeq G) . n) `1 ;
set w = LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n);
(LexBFS:CSeq G) . (n + 1) = LexBFS:Step ((LexBFS:CSeq G) . n) by Def17;
then (LexBFS:CSeq G) . (n + 1) = LexBFS:Update (((LexBFS:CSeq G) . n),(LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)),(card (dom (((LexBFS:CSeq G) . n) `1)))) by A1, Def14;
hence ((LexBFS:CSeq G) . (n + 1)) `1 = (((LexBFS:CSeq G) . n) `1) +* ((LexBFS:PickUnnumbered ((LexBFS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((LexBFS:CSeq G) . n) `1))))) by MCART_1:7; :: thesis: verum