let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is weak_SG-embedding & G2 is locally-finite holds
G1 is locally-finite
let F be PGraphMapping of G1,G2; :: thesis: ( F is weak_SG-embedding & G2 is locally-finite implies G1 is locally-finite )
assume A1: ( F is weak_SG-embedding & G2 is locally-finite ) ; :: thesis: G1 is locally-finite

now :: thesis: for v being Vertex of G1 holds v .degree() is finite

let v be Vertex of G1; :: thesis: v .degree() is finite
v .degree() c= ((F _V) /. v) .degree() by A1, GLIBPRE0:89;
hence v .degree() is finite by A1; :: thesis: verum

end;

hence G1 is locally-finite by Th23; :: thesis: verum