let G be finite _Graph; :: thesis: for n being Nat st card (dom (((MCS:CSeq G) . n) `1)) < G .order() holds
((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1)))))
let n be Nat; :: thesis: ( card (dom (((MCS:CSeq G) . n) `1)) < G .order() implies ((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1))))) )
assume A1: card (dom (((MCS:CSeq G) . n) `1)) < G .order() ; :: thesis: ((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1)))))
set CN1 = (MCS:CSeq G) . (n + 1);
set CSN = (MCS:CSeq G) . n;
set VLN = ((MCS:CSeq G) . n) `1 ;
set w = MCS:PickUnnumbered ((MCS:CSeq G) . n);
set k = (G .order()) -' (card (dom (((MCS:CSeq G) . n) `1)));
(MCS:CSeq G) . (n + 1) = MCS:Step ((MCS:CSeq G) . n) by Def26;
then (MCS:CSeq G) . (n + 1) = MCS:Update (((MCS:CSeq G) . n),(MCS:PickUnnumbered ((MCS:CSeq G) . n)),(card (dom (((MCS:CSeq G) . n) `1)))) by A1, Def23;
then consider L being MCS:Labeling of G such that
A2: L = [((((MCS:CSeq G) . n) `1) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1)))))),(((MCS:CSeq G) . n) `2)] and
A3: (MCS:CSeq G) . (n + 1) = MCS:LabelAdjacent (L,(MCS:PickUnnumbered ((MCS:CSeq G) . n))) by Def22;
((MCS:CSeq G) . (n + 1)) `1 = L `1 by A3, MCART_1:def 1;
hence ((MCS:CSeq G) . (n + 1)) `1 = (((MCS:CSeq G) . n) `1) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order()) -' (card (dom (((MCS:CSeq G) . n) `1))))) by A2, MCART_1:def 1; :: thesis: verum