let G1, G2 be Graph-yielding Function; :: thesis: ( dom G1 = dom F & ( for x being Element of dom F holds G1 . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) & dom G2 = dom F & ( for x being Element of dom F holds G2 . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) implies G1 = G2 )
assume that
A3: ( dom G1 = dom F & ( for x being Element of dom F holds G1 . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) ) and
A4: ( dom G2 = dom F & ( for x being Element of dom F holds G2 . x = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) ) ) ; :: thesis: G1 = G2

now :: thesis: for z being object st z in dom G1 holds
G1 . z = G2 . z

let z be object ; :: thesis: ( z in dom G1 implies G1 . z = G2 . z )
assume z in dom G1 ; :: thesis: G1 . z = G2 . z
then reconsider x = z as Element of dom F by A3;
thus G1 . z = replaceVerticesEdges ((renameElementsDistinctlyFunc ((the_Vertices_of F),x)),(renameElementsDistinctlyFunc ((the_Edges_of F),x))) by A3
.= G2 . z by A4 ; :: thesis: verum

end;

hence G1 = G2 by A3, A4, FUNCT_1:2; :: thesis: verum