for R, S being Relation st R is well-ordering holds
for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds
F = G