let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 holds F is PGraphMapping of dom F,G2
let F be PGraphMapping of G1,G2; :: thesis: F is PGraphMapping of dom F,G2
F = F | (dom F) by Th86;
hence F is PGraphMapping of dom F,G2 ; :: thesis: verum