let G1, G2 be _Graph; :: thesis:
let F be PGraphMapping of G1,G2; :: thesis:
let H be Subgraph of G1; :: thesis:
let F9 be PGraphMapping of H, rng (F | H); :: thesis:
assume A1: F9 = F | H ; :: thesis:

hereby :: thesis:

assume F is weak_SG-embedding ; :: thesis:
then ( F9 is total & F9 is one-to-one ) by A1, Th112;
hence F9 is weak_SG-embedding ; :: thesis:

end;

hereby :: thesis:

assume A2: F is strong_SG-embedding ; :: thesis:
then F9 is total by A1, Th112;
then ( F9 is total & F9 is one-to-one & F9 is continuous & F9 is onto ) by A1, A2, Th112;
hence F9 is isomorphism ; :: thesis:

end;

hereby :: thesis:

assume A3: ( F is directed & F is strong_SG-embedding ) ; :: thesis:
then F9 is total by A1, Th112;
then ( F9 is directed & F9 is total & F9 is one-to-one & F9 is continuous & F9 is onto ) by A1, A3, Th112;
hence F9 is Disomorphism ; :: thesis:

end;