let G1, G2 be _Graph; :: thesis: for F being semi-continuous PGraphMapping of G1,G2 st F is total & F is onto holds
F _V is continuous PVertexMapping of G1,G2
let F be semi-continuous PGraphMapping of G1,G2; :: thesis: ( F is total & F is onto implies F _V is continuous PVertexMapping of G1,G2 )
assume ( F is total & F is onto ) ; :: thesis: F _V is continuous PVertexMapping of G1,G2
then ( dom (F _E) = the_Edges_of G1 & rng (F _E) = the_Edges_of G2 ) by GLIB_010:def 11, GLIB_010:def 12;
hence F _V is continuous PVertexMapping of G1,G2 by Th23; :: thesis: verum