let G be _Graph; :: thesis: for v being set holds
( dom ((LexBFS:Init G) `2) = the_Vertices_of G & ((LexBFS:Init G) `2) . v = {} )
let v be set ; :: thesis: ( dom ((LexBFS:Init G) `2) = the_Vertices_of G & ((LexBFS:Init G) `2) . v = {} )
set g = (the_Vertices_of G) --> {};
set f = (the_Vertices_of G) --> {};
thus dom ((LexBFS:Init G) `2) = the_Vertices_of G by FUNCT_2:def 1; :: thesis: ((LexBFS:Init G) `2) . v = {}

A1: now :: thesis: for x being set holds ((the_Vertices_of G) --> {}) . x = {}

let x be set ; :: thesis: ((the_Vertices_of G) --> {}) . b₁ = {}

per cases ( x in dom ((the_Vertices_of G) --> {}) or not x in dom ((the_Vertices_of G) --> {}) ) ;

suppose x in dom ((the_Vertices_of G) --> {}) ; :: thesis: ((the_Vertices_of G) --> {}) . b₁ = {}

hence ((the_Vertices_of G) --> {}) . x = {} by FUNCOP_1:7; :: thesis: verum

end;

suppose not x in dom ((the_Vertices_of G) --> {}) ; :: thesis: ((the_Vertices_of G) --> {}) . b₁ = {}

hence ((the_Vertices_of G) --> {}) . x = {} by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

thus ((LexBFS:Init G) `2) . v = {} by A1; :: thesis: verum