let G1, G2 be _Graph; :: thesis: for F being non empty PGraphMapping of G1,G2 holds
( the_Vertices_of (dom F) = dom (F _V) & the_Edges_of (dom F) = dom (F _E) & the_Vertices_of (rng F) = rng (F _V) & the_Edges_of (rng F) = rng (F _E) )
let F be non empty PGraphMapping of G1,G2; :: thesis: ( the_Vertices_of (dom F) = dom (F _V) & the_Edges_of (dom F) = dom (F _E) & the_Vertices_of (rng F) = rng (F _V) & the_Edges_of (rng F) = rng (F _E) )
dom (F _E) c= G1 .edgesBetween (dom (F _V)) by Th7;
hence ( the_Vertices_of (dom F) = dom (F _V) & the_Edges_of (dom F) = dom (F _E) ) by GLIB_000:def 37; :: thesis: ( the_Vertices_of (rng F) = rng (F _V) & the_Edges_of (rng F) = rng (F _E) )
rng (F _E) c= G2 .edgesBetween (rng (F _V)) by Th7;
hence ( the_Vertices_of (rng F) = rng (F _V) & the_Edges_of (rng F) = rng (F _E) ) by GLIB_000:def 37; :: thesis: verum