let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is onto holds
( ( G1 is vertex-finite implies G2 is vertex-finite ) & ( G1 is edge-finite implies G2 is edge-finite ) )
let F be PGraphMapping of G1,G2; :: thesis: ( F is onto implies ( ( G1 is vertex-finite implies G2 is vertex-finite ) & ( G1 is edge-finite implies G2 is edge-finite ) ) )
assume A1: F is onto ; :: thesis: ( ( G1 is vertex-finite implies G2 is vertex-finite ) & ( G1 is edge-finite implies G2 is edge-finite ) )
hereby :: thesis: ( G1 is edge-finite implies G2 is edge-finite )
assume A2: G1 is vertex-finite ; :: thesis: G2 is vertex-finite
dom (F _V) is finite by A2;
then rng (F _V) is finite by FINSET_1:8;
hence G2 is vertex-finite by A1, GLIB_010:def 12; :: thesis: verum
end;
assume G1 is edge-finite ; :: thesis: G2 is edge-finite
then dom (F _E) is finite ;
then rng (F _E) is finite by FINSET_1:8;
hence G2 is edge-finite by A1, GLIB_010:def 12; :: thesis: verum