let G be finite _Graph; :: thesis: for n being Nat st n < G .order() holds
ex w being Vertex of G st
( w = MCS:PickUnnumbered ((MCS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((MCS:CSeq G) . n) `1 ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = ((((MCS:CSeq G) . n) `2 ) . v) + 1 ) & ( ( not v in G .AdjacentSet {w} or v in dom (((MCS:CSeq G) . n) `1 ) ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = (((MCS:CSeq G) . n) `2 ) . v ) ) ) )
let n be Nat; :: thesis: ( n < G .order() implies ex w being Vertex of G st
( w = MCS:PickUnnumbered ((MCS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((MCS:CSeq G) . n) `1 ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = ((((MCS:CSeq G) . n) `2 ) . v) + 1 ) & ( ( not v in G .AdjacentSet {w} or v in dom (((MCS:CSeq G) . n) `1 ) ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = (((MCS:CSeq G) . n) `2 ) . v ) ) ) ) )
assume A1: n < G .order() ; :: thesis: ex w being Vertex of G st
( w = MCS:PickUnnumbered ((MCS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {w} & not v in dom (((MCS:CSeq G) . n) `1 ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = ((((MCS:CSeq G) . n) `2 ) . v) + 1 ) & ( ( not v in G .AdjacentSet {w} or v in dom (((MCS:CSeq G) . n) `1 ) ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = (((MCS:CSeq G) . n) `2 ) . v ) ) ) )
set CSN = (MCS:CSeq G) . n;
set VLN = ((MCS:CSeq G) . n) `1 ;
set V2N = ((MCS:CSeq G) . n) `2 ;
set CN1 = (MCS:CSeq G) . (n + 1);
set V21 = ((MCS:CSeq G) . (n + 1)) `2 ;
set w = MCS:PickUnnumbered ((MCS:CSeq G) . n);
set k = (G .order() ) -' n;
A2: n = card (dom (((MCS:CSeq G) . n) `1 )) by A1, Th82;
set CSlv = [((((MCS:CSeq G) . n) `1 ) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n))),(((MCS:CSeq G) . n) `2 )];
set CSlv1 = (((MCS:CSeq G) . n) `1 ) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n));
d1: dom ((((MCS:CSeq G) . n) `1 ) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n))) = (dom (((MCS:CSeq G) . n) `1 )) \/ {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by Tw0;
r1: rng ((((MCS:CSeq G) . n) `1 ) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n))) c= (rng (((MCS:CSeq G) . n) `1 )) \/ (rng ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n))) by FUNCT_4:18;
rng ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n)) = {((G .order() ) -' n)} by FUNCOP_1:14;
then (rng (((MCS:CSeq G) . n) `1 )) \/ (rng ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n))) c= NAT by XBOOLE_1:8;
then rng ((((MCS:CSeq G) . n) `1 ) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n))) c= NAT by r1, XBOOLE_1:1;
then A2a: (((MCS:CSeq G) . n) `1 ) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n)) in PFuncs (the_Vertices_of G),NAT by d1, PARTFUN1:def 5;
reconsider CSlv = [((((MCS:CSeq G) . n) `1 ) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n))),(((MCS:CSeq G) . n) `2 )] as MCS:Labeling of G by A2a, ZFMISC_1:def 2;
A5: (MCS:CSeq G) . (n + 1) = MCS:Step ((MCS:CSeq G) . n) by Def40
.= MCS:Update ((MCS:CSeq G) . n),(MCS:PickUnnumbered ((MCS:CSeq G) . n)),n by A1, A2, Def39
.= MCS:LabelAdjacent CSlv,(MCS:PickUnnumbered ((MCS:CSeq G) . n)) by dLMCSU ;
set VLv = CSlv `1 ;
set V2v = CSlv `2 ;
CSlv `1 = (((MCS:CSeq G) . n) `1 ) +* ((MCS:PickUnnumbered ((MCS:CSeq G) . n)) .--> ((G .order() ) -' n)) by MCART_1:def 1;
then A8: dom (CSlv `1 ) = (dom (((MCS:CSeq G) . n) `1 )) \/ {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by Tw0;
A9: CSlv `2 = ((MCS:CSeq G) . n) `2 by MCART_1:def 2;
A10: dom (((MCS:CSeq G) . n) `1 ) c= dom (CSlv `1 ) by A8, XBOOLE_1:7;
A11: dom (((MCS:CSeq G) . n) `2 ) = the_Vertices_of G by FUNCT_2:def 1;

A12: now

let v be set ; :: thesis: ( v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} & not v in dom (((MCS:CSeq G) . n) `1 ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = ((((MCS:CSeq G) . n) `2 ) . v) + 1 )
assume A13: ( v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} & not v in dom (((MCS:CSeq G) . n) `1 ) ) ; :: thesis: (((MCS:CSeq G) . (n + 1)) `2 ) . v = ((((MCS:CSeq G) . n) `2 ) . v) + 1
not v in {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} by A13, CHORD:49;
then not v in dom (CSlv `1 ) by A8, A13, XBOOLE_0:def 3;
hence (((MCS:CSeq G) . (n + 1)) `2 ) . v = ((((MCS:CSeq G) . n) `2 ) . v) + 1 by A5, A9, A13, Th76, A11; :: thesis: verum

end;

A16: now

let v be set ; :: thesis: ( ( not v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} or v in dom (((MCS:CSeq G) . n) `1 ) ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . b₁ = (((MCS:CSeq G) . n) `2 ) . b<sub>1</sub> )
assume A17: ( not v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} or v in dom (((MCS:CSeq G) . n) `1 ) ) ; :: thesis: (((MCS:CSeq G) . (n + 1)) `2 ) . b<sub>1</sub> = (((MCS:CSeq G) . n) `2 ) . b₁

per cases ( not v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} or v in dom (((MCS:CSeq G) . n) `1 ) ) by A17;

suppose not v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} ; :: thesis: (((MCS:CSeq G) . (n + 1)) `2 ) . b<sub>1</sub> = (((MCS:CSeq G) . n) `2 ) . b₁

hence (((MCS:CSeq G) . (n + 1)) `2 ) . v = (((MCS:CSeq G) . n) `2 ) . v by A5, A9, Th74; :: thesis: verum

end;

suppose v in dom (((MCS:CSeq G) . n) `1 ) ; :: thesis: (((MCS:CSeq G) . (n + 1)) `2 ) . b₁ = (((MCS:CSeq G) . n) `2 ) . b₁

hence (((MCS:CSeq G) . (n + 1)) `2 ) . v = (((MCS:CSeq G) . n) `2 ) . v by A5, A9, A10, Th75; :: thesis: verum

end;

end;

end;

take MCS:PickUnnumbered ((MCS:CSeq G) . n) ; :: thesis: ( MCS:PickUnnumbered ((MCS:CSeq G) . n) = MCS:PickUnnumbered ((MCS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} & not v in dom (((MCS:CSeq G) . n) `1 ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = ((((MCS:CSeq G) . n) `2 ) . v) + 1 ) & ( ( not v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} or v in dom (((MCS:CSeq G) . n) `1 ) ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = (((MCS:CSeq G) . n) `2 ) . v ) ) ) )
thus ( MCS:PickUnnumbered ((MCS:CSeq G) . n) = MCS:PickUnnumbered ((MCS:CSeq G) . n) & ( for v being set holds
( ( v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} & not v in dom (((MCS:CSeq G) . n) `1 ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = ((((MCS:CSeq G) . n) `2 ) . v) + 1 ) & ( ( not v in G .AdjacentSet {(MCS:PickUnnumbered ((MCS:CSeq G) . n))} or v in dom (((MCS:CSeq G) . n) `1 ) ) implies (((MCS:CSeq G) . (n + 1)) `2 ) . v = (((MCS:CSeq G) . n) `2 ) . v ) ) ) ) by A12, A16; :: thesis: verum