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

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

hence
R |_2 Z,S |_2 (F .: Z) are_isomorphic
; :: thesis: verum
thus A9:
dom (F | Z) = field (R |_2 Z)
by A2, A8, A7, RELAT_1:62; :: 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 A5, RELAT_1:115; :: 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 A6, FUNCT_1:52; :: 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 )

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 A9, A15, FUNCT_1:47;

then A17: [(F . a),(F . b)] in S by A16, XBOOLE_0:def 4;

A18: [a,b] in [:Z,Z:] by A7, A15, ZFMISC_1:87;

( a in field R & b in field R ) by A15, Th12;

then [a,b] in R by A3, A17;

hence [a,b] in R |_2 Z by A18, XBOOLE_0:def 4; :: thesis: verum

end;( [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 A5, RELAT_1:115; :: 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 A6, FUNCT_1:52; :: 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 that
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 A11, RELAT_1:15; :: 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 A9, FUNCT_1:def 3;

then A14: [((F | Z) . a),((F | Z) . b)] in [:(F .: Z),(F .: Z):] by A5, A10, ZFMISC_1:87;

( F . a = (F | Z) . a & F . b = (F | Z) . b ) by A9, A13, FUNCT_1:47;

hence [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) by A12, A14, XBOOLE_0:def 4; :: thesis: verum

end;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 A11, RELAT_1:15; :: 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 A9, FUNCT_1:def 3;

then A14: [((F | Z) . a),((F | Z) . b)] in [:(F .: Z),(F .: Z):] by A5, A10, ZFMISC_1:87;

( F . a = (F | Z) . a & F . b = (F | Z) . b ) by A9, A13, FUNCT_1:47;

hence [((F | Z) . a),((F | Z) . b)] in S |_2 (F .: Z) by A12, A14, XBOOLE_0:def 4; :: thesis: verum

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 A9, A15, FUNCT_1:47;

then A17: [(F . a),(F . b)] in S by A16, XBOOLE_0:def 4;

A18: [a,b] in [:Z,Z:] by A7, A15, ZFMISC_1:87;

( a in field R & b in field R ) by A15, Th12;

then [a,b] in R by A3, A17;

hence [a,b] in R |_2 Z by A18, XBOOLE_0:def 4; :: thesis: verum