:: deftheorem Def57b defines _finite GLIB_000:def 66 :
for GF being non empty Graph-yielding Function holds
( GF is _finite iff for x being Element of dom GF holds GF . x is _finite );