deffunc H₁( object ) -> plain _Graph = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),(In ($1,(dom F))))),(renameElementsDistinctlyFunc ((the_Edges_of F),(In ($1,(dom F))))));
consider g being Function such that
A1: dom g = dom F and
A2: for x being Element of dom F holds g . x = H₁(x) from FUNCT_1:sch 4();

now :: thesis: for x being object st x in dom g holds
g . x is _Graph

let x be object ; :: thesis: ( x in dom g implies g . x is _Graph )
assume x in dom g ; :: thesis: g . x is _Graph
then g . x = H₁(x) by A1, A2;
hence g . x is _Graph ; :: thesis: verum

end;

then reconsider g = g as Graph-yielding Function by GLIB_000:def 53;
take g ; :: thesis: ( dom g = dom F & ( for x being Element of dom F holds g . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) )
thus dom g = dom F by A1; :: thesis: for x being Element of dom F holds g . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x)))
let x be Element of dom F; :: thesis: g . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x)))
In (x,(dom F)) = x ;
hence g . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) by A2; :: thesis: verum