let G be _Graph; :: thesis: for v being Vertex of G holds Im ((VertexDomRel G),v) = v .outNeighbors()
let v be Vertex of G; :: thesis: Im ((VertexDomRel G),v) = v .outNeighbors()

now :: thesis: for x being object holds
( ( x in (VertexDomRel G) .: {v} implies x in v .outNeighbors() ) & ( x in v .outNeighbors() implies x in (VertexDomRel G) .: {v} ) )

let x be object ; :: thesis: ( ( x in (VertexDomRel G) .: {v} implies x in v .outNeighbors() ) & ( x in v .outNeighbors() implies x in (VertexDomRel G) .: {v} ) )

hereby :: thesis: ( x in v .outNeighbors() implies x in (VertexDomRel G) .: {v} )

assume x in (VertexDomRel G) .: {v} ; :: thesis: x in v .outNeighbors()
then consider v0 being object such that
A1: ( [v0,x] in VertexDomRel G & v0 in {v} ) by RELAT_1:def 13;
[v,x] in VertexDomRel G by A1, TARSKI:def 1;
then ( x is set & ex e being object st e DJoins v,x,G ) by Th1, TARSKI:1;
hence x in v .outNeighbors() by GLIB_000:70; :: thesis: verum

end;

assume x in v .outNeighbors() ; :: thesis: x in (VertexDomRel G) .: {v}
then ex e being object st e DJoins v,x,G by GLIB_000:70;
then ( [v,x] in VertexDomRel G & v in {v} ) by Th1, TARSKI:def 1;
hence x in (VertexDomRel G) .: {v} by RELAT_1:def 13; :: thesis: verum

end;

then (VertexDomRel G) .: {v} = v .outNeighbors() by TARSKI:2;
hence Im ((VertexDomRel G),v) = v .outNeighbors() by RELAT_1:def 16; :: thesis: verum