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

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