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

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:13; :: 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 4; :: thesis: verum

end;

end;

end;

(LexBFS:Init G) `2 = (the_Vertices_of G) --> {} by MCART_1:7;
hence ((LexBFS:Init G) `2 ) . v = {} by A1; :: thesis: verum