theorem Th48: :: WELLORD1:48

for Z being set
for R, S being Relation
for F being Function st R is well-ordering & Z c= field R & F is_isomorphism_of R,S holds
( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )