let G be finite _Graph; :: thesis: for L being LexBFS:Labeling of G
for v being Vertex of G
for x being set
for k being Nat st not x in G .AdjacentSet {v} holds
(L `2 ) . x = ((LexBFS:Update L,v,k) `2 ) . x
let L be LexBFS:Labeling of G; :: thesis: for v being Vertex of G
for x being set
for k being Nat st not x in G .AdjacentSet {v} holds
(L `2 ) . x = ((LexBFS:Update L,v,k) `2 ) . x
let v be Vertex of G; :: thesis: for x being set
for k being Nat st not x in G .AdjacentSet {v} holds
(L `2 ) . x = ((LexBFS:Update L,v,k) `2 ) . x
let x be set ; :: thesis: for k being Nat st not x in G .AdjacentSet {v} holds
(L `2 ) . x = ((LexBFS:Update L,v,k) `2 ) . x
let k be Nat; :: thesis: ( not x in G .AdjacentSet {v} implies (L `2 ) . x = ((LexBFS:Update L,v,k) `2 ) . x )
assume A1: not x in G .AdjacentSet {v} ; :: thesis: (L `2 ) . x = ((LexBFS:Update L,v,k) `2 ) . x
set F = ((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)};
dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)}) = (G .AdjacentSet {v}) \ (dom (L `1 )) by FUNCOP_1:19;
then A2: not x in dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)}) by A1, XBOOLE_0:def 5;
then A3: (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)}) . x = {} by FUNCT_1:def 4;
set L2 = (LexBFS:Update L,v,k) `2 ;
A4: (LexBFS:Update L,v,k) `2 = (L `2 ) .\/ (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)}) by MCART_1:7;

per cases ( x in dom (L `2 ) or not x in dom (L `2 ) ) ;

suppose x in dom (L `2 ) ; :: thesis: (L `2 ) . x = ((LexBFS:Update L,v,k) `2 ) . x

then x in (dom (L `2 )) \/ (dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)})) by XBOOLE_0:def 3;
hence ((LexBFS:Update L,v,k) `2 ) . x = ((L `2 ) . x) \/ ((((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)}) . x) by A4, Def2
.= (L `2 ) . x by A3 ;
:: thesis: verum

end;

suppose A5: not x in dom (L `2 ) ; :: thesis: (L `2 ) . x = ((LexBFS:Update L,v,k) `2 ) . x

then not x in (dom (L `2 )) \/ (dom (((G .AdjacentSet {v}) \ (dom (L `1 ))) --> {((G .order() ) -' k)})) by A2, XBOOLE_0:def 3;
then not x in dom ((LexBFS:Update L,v,k) `2 ) by A4, Def2;
hence ((LexBFS:Update L,v,k) `2 ) . x = {} by FUNCT_1:def 4
.= (L `2 ) . x by A5, FUNCT_1:def 4 ;
:: thesis: verum

end;

end;