let Z be set ; :: thesis: 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 )

let R, S be Relation; :: thesis: 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 )

let F be Function; :: thesis: ( R is well-ordering & Z c= field R & F is_isomorphism_of R,S implies ( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic ) )
assume that
A1: R is well-ordering and
A2: Z c= field R and
A3: F is_isomorphism_of R,S ; :: thesis: ( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
A4: F .: Z c= rng F by RELAT_1:111;
A5: F .: Z = field (S |_2 (F .: Z)) by A1, A3, A4, Th31, Th44;
A6: F is one-to-one by A3;
A7: Z = field (R |_2 Z) by A1, A2, Th31;
A8: dom F = field R by A3;
thus F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) :: thesis: R |_2 Z,S |_2 (F .: Z) are_isomorphic
proof
thus A9: dom (F | Z) = field (R |_2 Z) by ; :: according to WELLORD1:def 7 :: thesis: ( rng (F | Z) = field (S |_2 (F .: Z)) & F | Z is one-to-one & ( for a, b being object holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) ) )

thus A10: rng (F | Z) = field (S |_2 (F .: Z)) by ; :: thesis: ( F | Z is one-to-one & ( for a, b being object holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) ) )

thus F | Z is one-to-one by ; :: thesis: for a, b being object holds
( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) )

let a, b be object ; :: thesis: ( [a,b] in R |_2 Z iff ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) )
thus ( [a,b] in R |_2 Z implies ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ) ) :: thesis: ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) implies [a,b] in R |_2 Z )
proof
assume A11: [a,b] in R |_2 Z ; :: thesis: ( a in field (R |_2 Z) & b in field (R |_2 Z) & [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) )
then [a,b] in R by XBOOLE_0:def 4;
then A12: [(F . a),(F . b)] in S by A3;
thus A13: ( a in field (R |_2 Z) & b in field (R |_2 Z) ) by ; :: thesis: [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z)
then ( (F | Z) . a in rng (F | Z) & (F | Z) . b in rng (F | Z) ) by ;
then A14: [((F | Z) . a),((F | Z) . b)] in [:(F .: Z),(F .: Z):] by ;
( F . a = (F | Z) . a & F . b = (F | Z) . b ) by ;
hence [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) by ; :: thesis: verum
end;
assume that
A15: ( a in field (R |_2 Z) & b in field (R |_2 Z) ) and
A16: [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) ; :: thesis: [a,b] in R |_2 Z
( F . a = (F | Z) . a & F . b = (F | Z) . b ) by ;
then A17: [(F . a),(F . b)] in S by ;
A18: [a,b] in [:Z,Z:] by ;
( a in field R & b in field R ) by ;
then [a,b] in R by ;
hence [a,b] in R |_2 Z by ; :: thesis: verum
end;
hence R |_2 Z,S |_2 (F .: Z) are_isomorphic ; :: thesis: verum