theorem Th38: :: GLIB_015:38

for F1, F2 being non empty Graph-yielding Function st dom F1 = dom F2 & ( for x1 being Element of dom F1
for x2 being Element of dom F2 st x1 = x2 holds
F2 . x2 is F1 . x1 -Disomorphic ) holds
F1,F2 are_Disomorphic