let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is locally-finite iff G2 is locally-finite )
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( G1 is locally-finite iff G2 is locally-finite ) )
assume A1: F is isomorphism ; :: thesis: ( G1 is locally-finite iff G2 is locally-finite )
hereby :: thesis: ( G2 is locally-finite implies G1 is locally-finite )
assume A2: G1 is locally-finite ; :: thesis: G2 is locally-finite
now :: thesis: for v being Vertex of G2 holds v .degree() is finite
let v be Vertex of G2; :: thesis: v .degree() is finite
rng (F _V) = the_Vertices_of G2 by A1, GLIB_010:def 12;
then consider v0 being object such that
A3: ( v0 in dom (F _V) & (F _V) . v0 = v ) by FUNCT_1:def 3;
reconsider v0 = v0 as Vertex of G1 by A3;
((F _V) /. v0) .degree() = v0 .degree() by A1, GLIBPRE0:95;
hence v .degree() is finite by A2, A3, PARTFUN1:def 6; :: thesis: verum
end;
hence G2 is locally-finite by Th23; :: thesis: verum
end;
thus ( G2 is locally-finite implies G1 is locally-finite ) by A1, Th32; :: thesis: verum