take the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) ; :: thesis: for v, w being Vertex of G1 st v in dom the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) & w in dom the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) & v,w are_adjacent holds
the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) /. v, the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) /. w are_adjacent
thus for v, w being Vertex of G1 st v in dom the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) & w in dom the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) & v,w are_adjacent holds
the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) /. v, the empty PartFunc of (the_Vertices_of G1),(the_Vertices_of G2) /. w are_adjacent ; :: thesis: verum