let G1, G2 be _Graph; :: thesis: for F being one-to-one PGraphMapping of G1,G2 st F is total & F is continuous holds
F " is continuous
let F be one-to-one PGraphMapping of G1,G2; :: thesis: ( F is total & F is continuous implies F " is continuous )
assume ( F is total & F is continuous ) ; :: thesis: F " is continuous
then F " is onto by FUNCT_1:33;
hence F " is continuous ; :: thesis: verum