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

hereby :: thesis: ( G2 is edge-finite implies G1 is edge-finite )

assume A2: G2 is vertex-finite ; :: thesis: G1 is vertex-finite
( dom (F _V) = the_Vertices_of G1 & F _V is one-to-one ) by A1, GLIB_010:def 11;
then the_Vertices_of G1,(F _V) .: (the_Vertices_of G1) are_equipotent by CARD_1:33;
hence G1 is vertex-finite by A2, CARD_1:38; :: thesis: verum

end;

assume A3: G2 is edge-finite ; :: thesis: G1 is edge-finite
( dom (F _E) = the_Edges_of G1 & F _E is one-to-one ) by A1, GLIB_010:def 11;
then the_Edges_of G1,(F _E) .: (the_Edges_of G1) are_equipotent by CARD_1:33;
hence G1 is edge-finite by A3, CARD_1:38; :: thesis: verum