let G be finite _Graph; :: thesis: for n being Nat
for x being set st not x in dom (((MCS:CSeq G) . n) `1 ) holds
(((MCS:CSeq G) . n) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1 )))
let n be Nat; :: thesis: for x being set st not x in dom (((MCS:CSeq G) . n) `1 ) holds
(((MCS:CSeq G) . n) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1 )))
set CN = (MCS:CSeq G) . n;
set VLN = ((MCS:CSeq G) . n) `1 ;
set VL2 = ((MCS:CSeq G) . n) `2 ;
let x be set ; :: thesis: ( not x in dom (((MCS:CSeq G) . n) `1 ) implies (((MCS:CSeq G) . n) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1 ))) )
assume A1: not x in dom (((MCS:CSeq G) . n) `1 ) ; :: thesis: (((MCS:CSeq G) . n) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1 )))
defpred S₁[ Nat] means for x being set st not x in dom (((MCS:CSeq G) . $1) `1 ) holds
(((MCS:CSeq G) . $1) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . $1) `1 )));

now

let x be set ; :: thesis: ( not x in dom (((MCS:CSeq G) . 0 ) `1 ) implies (((MCS:CSeq G) . 0 ) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . 0 ) `1 ))) )
set C0 = (MCS:CSeq G) . 0 ;
set VL0 = ((MCS:CSeq G) . 0 ) `1 ;
set V20 = ((MCS:CSeq G) . 0 ) `2 ;
assume not x in dom (((MCS:CSeq G) . 0 ) `1 ) ; :: thesis: (((MCS:CSeq G) . 0 ) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . 0 ) `1 )))
A2: (MCS:CSeq G) . 0 = MCS:Init G by Def40;
then dom (((MCS:CSeq G) . 0 ) `1 ) = {} by MCART_1:def 1, RELAT_1:60;
hence (((MCS:CSeq G) . 0 ) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . 0 ) `1 ))) by A2, Th70, CARD_1:47; :: thesis: verum

end;

then A3: S₁[ 0 ] ;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
set CSK = (MCS:CSeq G) . k;
set VLK = ((MCS:CSeq G) . k) `1 ;
set VK2 = ((MCS:CSeq G) . k) `2 ;
set CS1 = (MCS:CSeq G) . (k + 1);
set VL1 = ((MCS:CSeq G) . (k + 1)) `1 ;
set V12 = ((MCS:CSeq G) . (k + 1)) `2 ;
A6: k <= k + 1 by XREAL_1:40;

per cases ( G .order() <= k or k < G .order() ) ;

suppose G .order() <= k ; :: thesis: S₁[k + 1]

then ( ((MCS:CSeq G) . k) `1 = ((MCS:CSeq G) . (k + 1)) `1 & ((MCS:CSeq G) . k) `2 = ((MCS:CSeq G) . (k + 1)) `2 ) by A6, Th84;
hence S₁[k + 1] by A5; :: thesis: verum

end;

suppose A7: k < G .order() ; :: thesis: S₁[k + 1]

then consider w being Vertex of G such that
A8: w = MCS:PickUnnumbered ((MCS:CSeq G) . k) and
A9: for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((MCS:CSeq G) . k) `1 ) implies (((MCS:CSeq G) . (k + 1)) `2 ) . v = ((((MCS:CSeq G) . k) `2 ) . v) + 1 ) & ( ( not v in G .AdjacentSet {w} or v in dom (((MCS:CSeq G) . k) `1 ) ) implies (((MCS:CSeq G) . (k + 1)) `2 ) . v = (((MCS:CSeq G) . k) `2 ) . v ) ) by Th90;
A10: G .order() = (MCS:CSeq G) .Lifespan() by Th87;
set VL = (MCS:CSeq G) ``1 ;
A4a: ( ((MCS:CSeq G) . k) `1 = ((MCS:CSeq G) ``1 ) . k & ((MCS:CSeq G) . (k + 1)) `1 = ((MCS:CSeq G) ``1 ) . (k + 1) ) by d1stMCSLS;
A4b: (MCS:CSeq G) .Lifespan() = ((MCS:CSeq G) ``1 ) .Lifespan() by mVNS0;
w = ((MCS:CSeq G) ``1 ) .PickedAt k by A7, A8, Th89;
then A11: dom (((MCS:CSeq G) . (k + 1)) `1 ) = (dom (((MCS:CSeq G) . k) `1 )) \/ {w} by A4a, A4b, A7, A10, Th18;

now

let x be set ; :: thesis: ( not x in dom (((MCS:CSeq G) . (k + 1)) `1 ) implies card ((G .AdjacentSet {b<sub>1</sub>}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1 ))) = (((MCS:CSeq G) . (k + 1)) `2 ) . b<sub>1</sub> )
assume A12: not x in dom (((MCS:CSeq G) . (k + 1)) `1 ) ; :: thesis: card ((G .AdjacentSet {b₁}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1 ))) = (((MCS:CSeq G) . (k + 1)) `2 ) . b₁
A13: not x in dom (((MCS:CSeq G) . k) `1 ) by A11, A12, XBOOLE_0:def 3;
then A14: card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1 ))) = (((MCS:CSeq G) . k) `2 ) . x by A5;

per cases ( ( x in G .AdjacentSet {w} & not x in dom (((MCS:CSeq G) . k) `1 ) ) or not x in G .AdjacentSet {w} or x in dom (((MCS:CSeq G) . k) `1 ) ) ;

suppose A15: ( x in G .AdjacentSet {w} & not x in dom (((MCS:CSeq G) . k) `1 ) ) ; :: thesis: card ((G .AdjacentSet {b<sub>1</sub>}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1 ))) = (((MCS:CSeq G) . (k + 1)) `2 ) . b₁

then A16: (((MCS:CSeq G) . (k + 1)) `2 ) . x = ((((MCS:CSeq G) . k) `2 ) . x) + 1 by A9;
set GAS = G .AdjacentSet {x};
A17: w in G .AdjacentSet {x} by A15, CHORD:53;
dom (((MCS:CSeq G) . k) `1 ) <> the_Vertices_of G by A7, Th86;
then not w in dom (((MCS:CSeq G) . k) `1 ) by A8, Th73;
then A19: not w in (G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1 )) by XBOOLE_0:def 4;
A20: {w} c= G .AdjacentSet {x} by A17, ZFMISC_1:37;
(G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1 )) = ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1 ))) \/ ((G .AdjacentSet {x}) /\ {w}) by A11, XBOOLE_1:23
.= ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1 ))) \/ {w} by A20, XBOOLE_1:28 ;
hence card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1 ))) = (((MCS:CSeq G) . (k + 1)) `2 ) . x by A14, A16, A19, CARD_2:54; :: thesis: verum

end;

suppose A21: ( not x in G .AdjacentSet {w} or x in dom (((MCS:CSeq G) . k) `1 ) ) ; :: thesis: card ((G .AdjacentSet {b<sub>1</sub>}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1 ))) = (((MCS:CSeq G) . (k + 1)) `2 ) . b₁

then A22: (((MCS:CSeq G) . (k + 1)) `2 ) . x = (((MCS:CSeq G) . k) `2 ) . x by A9;
set GAS = G .AdjacentSet {x};
A23: not w in G .AdjacentSet {x} by A11, A12, A21, CHORD:53, XBOOLE_0:def 3;
(G .AdjacentSet {x}) /\ {w} c= {w} by XBOOLE_1:17;
then (G .AdjacentSet {x}) /\ {w} in bool {w} ;
then A24: (G .AdjacentSet {x}) /\ {w} in {{} ,{w}} by ZFMISC_1:30;

A25: now

assume (G .AdjacentSet {x}) /\ {w} = {w} ; :: thesis: contradiction
then w in (G .AdjacentSet {x}) /\ {w} by TARSKI:def 1;
hence contradiction by A23, XBOOLE_0:def 4; :: thesis: verum

end;

(G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1 )) = ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1 ))) \/ ((G .AdjacentSet {x}) /\ {w}) by A11, XBOOLE_1:23
.= ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1 ))) \/ {} by A24, A25, TARSKI:def 2
.= (G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . k) `1 )) ;
hence card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . (k + 1)) `1 ))) = (((MCS:CSeq G) . (k + 1)) `2 ) . x by A5, A13, A22; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A3, A4);
hence (((MCS:CSeq G) . n) `2 ) . x = card ((G .AdjacentSet {x}) /\ (dom (((MCS:CSeq G) . n) `1 ))) by A1; :: thesis: verum