for F1, F2 being non empty one-to-one Graph-yielding Function st F1,F2 are_Disomorphic holds
rng F1, rng F2 are_Disomorphic