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 x in dom (L `1) holds

((LexBFS:Update (L,v,k)) `2) . x = (L `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 x in dom (L `1) holds

((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x

let v be Vertex of G; :: thesis: for x being set

for k being Nat st x in dom (L `1) holds

((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x

let x be set ; :: thesis: for k being Nat st x in dom (L `1) holds

((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x

let k be Nat; :: thesis: ( x in dom (L `1) implies ((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x )

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

set F = ((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' k)};

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 2;

set L2 = (LexBFS:Update (L,v,k)) `2 ;

for v being Vertex of G

for x being set

for k being Nat st x in dom (L `1) holds

((LexBFS:Update (L,v,k)) `2) . x = (L `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 x in dom (L `1) holds

((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x

let v be Vertex of G; :: thesis: for x being set

for k being Nat st x in dom (L `1) holds

((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x

let x be set ; :: thesis: for k being Nat st x in dom (L `1) holds

((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x

let k be Nat; :: thesis: ( x in dom (L `1) implies ((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x )

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

set F = ((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' k)};

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 2;

set L2 = (LexBFS:Update (L,v,k)) `2 ;

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

end;

suppose
x in dom (L `2)
; :: thesis: ((LexBFS:Update (L,v,k)) `2) . x = (L `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 Def1

.= (L `2) . x by A3 ;

:: thesis: verum

end;hence ((LexBFS:Update (L,v,k)) `2) . x = ((L `2) . x) \/ ((((G .AdjacentSet {v}) \ (dom (L `1))) --> {((G .order()) -' k)}) . x) by Def1

.= (L `2) . x by A3 ;

:: thesis: verum

suppose A4:
not x in dom (L `2)
; :: thesis: ((LexBFS:Update (L,v,k)) `2) . x = (L `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 Def1;

hence ((LexBFS:Update (L,v,k)) `2) . x = {} by FUNCT_1:def 2

.= (L `2) . x by A4, FUNCT_1:def 2 ;

:: thesis: verum

end;then not x in dom ((LexBFS:Update (L,v,k)) `2) by Def1;

hence ((LexBFS:Update (L,v,k)) `2) . x = {} by FUNCT_1:def 2

.= (L `2) . x by A4, FUNCT_1:def 2 ;

:: thesis: verum