let G be _finite _Graph; 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; 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; 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 ; 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; ( x in dom (L `1) implies ((LexBFS:Update (L,v,k)) `2) . x = (L `2) . x )
assume A1:
x in dom (L `1)
; ((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 ;