let R, S be Relation; :: thesis: ( R is well-ordering & S is well-ordering & not R,S are_isomorphic & ( for a being object holds

( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) implies ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

assume that

A1: R is well-ordering and

A2: S is well-ordering ; :: thesis: ( R,S are_isomorphic or ex a being object st

( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

defpred S_{1}[ object ] means ex b being object st

( b in field S & R |_2 (R -Seg $1),S |_2 (S -Seg b) are_isomorphic );

consider Z being set such that

A3: for a being object holds

( a in Z iff ( a in field R & S_{1}[a] ) )
from XBOOLE_0:sch 1();

A4: Z c= field R by A3;

defpred S_{2}[ object , object ] means ( $2 in field S & R |_2 (R -Seg $1),S |_2 (S -Seg $2) are_isomorphic );

A5: for a, b, c being object st S_{2}[a,b] & S_{2}[a,c] holds

b = c

A9: for a, b being object holds

( [a,b] in F iff ( a in field R & S_{2}[a,b] ) )
from FUNCT_1:sch 1(A5);

A10: Z = dom F

( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) ) by A1, A2, A4, A15, A66, A87, A61, A83, A105, Th28; :: thesis: verum

( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) implies ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

assume that

A1: R is well-ordering and

A2: S is well-ordering ; :: thesis: ( R,S are_isomorphic or ex a being object st

( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

defpred S

( b in field S & R |_2 (R -Seg $1),S |_2 (S -Seg b) are_isomorphic );

consider Z being set such that

A3: for a being object holds

( a in Z iff ( a in field R & S

A4: Z c= field R by A3;

defpred S

A5: for a, b, c being object st S

b = c

proof

consider F being Function such that
let a, b, c be object ; :: thesis: ( S_{2}[a,b] & S_{2}[a,c] implies b = c )

assume that

A6: b in field S and

A7: R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic and

A8: ( c in field S & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic ) ; :: thesis: b = c

S |_2 (S -Seg b),R |_2 (R -Seg a) are_isomorphic by A7, Th40;

hence b = c by A2, A6, A8, Th42, Th47; :: thesis: verum

end;assume that

A6: b in field S and

A7: R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic and

A8: ( c in field S & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic ) ; :: thesis: b = c

S |_2 (S -Seg b),R |_2 (R -Seg a) are_isomorphic by A7, Th40;

hence b = c by A2, A6, A8, Th42, Th47; :: thesis: verum

A9: for a, b being object holds

( [a,b] in F iff ( a in field R & S

A10: Z = dom F

proof

A15:
rng F c= field S
thus
for a being object st a in Z holds

a in dom F :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom F c= Z

assume a in dom F ; :: thesis: a in Z

then consider b being object such that

A13: [a,b] in F by XTUPLE_0:def 12;

A14: R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic by A9, A13;

( a in field R & b in field S ) by A9, A13;

hence a in Z by A3, A14; :: thesis: verum

end;a in dom F :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: dom F c= Z

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in dom F or a in Z )
let a be object ; :: thesis: ( a in Z implies a in dom F )

assume A11: a in Z ; :: thesis: a in dom F

then consider b being object such that

A12: ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A3;

a in field R by A3, A11;

then [a,b] in F by A9, A12;

hence a in dom F by XTUPLE_0:def 12; :: thesis: verum

end;assume A11: a in Z ; :: thesis: a in dom F

then consider b being object such that

A12: ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A3;

a in field R by A3, A11;

then [a,b] in F by A9, A12;

hence a in dom F by XTUPLE_0:def 12; :: thesis: verum

assume a in dom F ; :: thesis: a in Z

then consider b being object such that

A13: [a,b] in F by XTUPLE_0:def 12;

A14: R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic by A9, A13;

( a in field R & b in field S ) by A9, A13;

hence a in Z by A3, A14; :: thesis: verum

proof

A17:
F is_isomorphism_of R |_2 (dom F),S |_2 (rng F)
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng F or a in field S )

assume a in rng F ; :: thesis: a in field S

then consider b being object such that

A16: ( b in dom F & a = F . b ) by FUNCT_1:def 3;

[b,a] in F by A16, FUNCT_1:1;

hence a in field S by A9; :: thesis: verum

end;assume a in rng F ; :: thesis: a in field S

then consider b being object such that

A16: ( b in dom F & a = F . b ) by FUNCT_1:def 3;

[b,a] in F by A16, FUNCT_1:1;

hence a in field S by A9; :: thesis: verum

proof

thus
( dom F = field (R |_2 (dom F)) & rng F = field (S |_2 (rng F)) )
by A1, A2, A4, A15, A10, Th31; :: according to WELLORD1:def 7 :: thesis: ( F is one-to-one & ( for a, b being object holds

( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) ) ) )

thus A18: F is one-to-one :: thesis: for a, b being object holds

( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) )

set P = R |_2 (R -Seg a);

A25: ( field (R |_2 (R -Seg a)) = R -Seg a & R |_2 (R -Seg a) is well-ordering ) by A1, Th25, Th32;

thus ( [a,b] in R |_2 (dom F) implies ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) ) :: thesis: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) implies [a,b] in R |_2 (dom F) )

A43: a in field (R |_2 (dom F)) and

A44: b in field (R |_2 (dom F)) and

A45: [(F . a),(F . b)] in S |_2 (rng F) ; :: thesis: [a,b] in R |_2 (dom F)

A46: [(F . a),(F . b)] in S by A45, XBOOLE_0:def 4;

A47: a in dom F by A43, Th12;

then A48: [a,(F . a)] in F by FUNCT_1:1;

then A49: a in field R by A9;

assume not [a,b] in R |_2 (dom F) ; :: thesis: contradiction

then A50: ( not [a,b] in R or not [a,b] in [:(dom F),(dom F):] ) by XBOOLE_0:def 4;

then A51: a <> b by A1, A47, A49, Lm1, ZFMISC_1:87;

A52: b in dom F by A44, Th12;

then A53: [b,(F . b)] in F by FUNCT_1:1;

then A54: R |_2 (R -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by A9;

A55: b in field R by A9, A53;

then A56: [b,a] in R by A1, A47, A52, A50, A49, A51, Lm4, ZFMISC_1:87;

then A57: R -Seg b c= R -Seg a by A1, A49, A55, Th29;

A58: b in R -Seg a by A47, A52, A50, A56, Th1, ZFMISC_1:87;

then (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, Th27;

then A59: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by A54, A57, Th22;

A60: F . b in field S by A9, A53;

( F . a in field S & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by A9, A48;

then [(F . b),(F . a)] in S by A2, A60, A58, A25, A59, Th51;

then F . a = F . b by A2, A46, Lm3;

hence contradiction by A18, A47, A52, A51; :: thesis: verum

end;( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) ) ) )

thus A18: F is one-to-one :: thesis: for a, b being object holds

( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) )

proof

let a, b be object ; :: thesis: ( [a,b] in R |_2 (dom F) iff ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) )
let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( not a in dom F or not b in dom F or not F . a = F . b or a = b )

assume that

A19: a in dom F and

A20: b in dom F and

A21: F . a = F . b ; :: thesis: a = b

A22: [b,(F . b)] in F by A20, FUNCT_1:1;

then R |_2 (R -Seg b),S |_2 (S -Seg (F . a)) are_isomorphic by A9, A21;

then A23: S |_2 (S -Seg (F . a)),R |_2 (R -Seg b) are_isomorphic by Th40;

[a,(F . a)] in F by A19, FUNCT_1:1;

then A24: ( a in field R & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by A9;

b in field R by A9, A22;

hence a = b by A1, A24, A23, Th42, Th47; :: thesis: verum

end;assume that

A19: a in dom F and

A20: b in dom F and

A21: F . a = F . b ; :: thesis: a = b

A22: [b,(F . b)] in F by A20, FUNCT_1:1;

then R |_2 (R -Seg b),S |_2 (S -Seg (F . a)) are_isomorphic by A9, A21;

then A23: S |_2 (S -Seg (F . a)),R |_2 (R -Seg b) are_isomorphic by Th40;

[a,(F . a)] in F by A19, FUNCT_1:1;

then A24: ( a in field R & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by A9;

b in field R by A9, A22;

hence a = b by A1, A24, A23, Th42, Th47; :: thesis: verum

set P = R |_2 (R -Seg a);

A25: ( field (R |_2 (R -Seg a)) = R -Seg a & R |_2 (R -Seg a) is well-ordering ) by A1, Th25, Th32;

thus ( [a,b] in R |_2 (dom F) implies ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) ) ) :: thesis: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) implies [a,b] in R |_2 (dom F) )

proof

assume that
assume A26:
[a,b] in R |_2 (dom F)
; :: thesis: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) & [(F . a),(F . b)] in S |_2 (rng F) )

hence A27: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) ) by RELAT_1:15; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)

then A28: a in dom F by Th12;

then A29: [a,(F . a)] in F by FUNCT_1:1;

then A30: F . a in field S by A9;

A31: b in dom F by A27, Th12;

then A32: [b,(F . b)] in F by FUNCT_1:1;

then A33: b in field R by A9;

A34: ( F . b in field S & R |_2 (R -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic ) by A9, A32;

A35: [a,b] in R by A26, XBOOLE_0:def 4;

A36: F . b in rng F by A31, FUNCT_1:def 3;

F . a in rng F by A28, FUNCT_1:def 3;

then A37: [(F . a),(F . b)] in [:(rng F),(rng F):] by A36, ZFMISC_1:87;

a in field R by A9, A29;

then A38: R -Seg a c= R -Seg b by A1, A33, A35, Th29;

A39: R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by A9, A29;

end;hence A27: ( a in field (R |_2 (dom F)) & b in field (R |_2 (dom F)) ) by RELAT_1:15; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)

then A28: a in dom F by Th12;

then A29: [a,(F . a)] in F by FUNCT_1:1;

then A30: F . a in field S by A9;

A31: b in dom F by A27, Th12;

then A32: [b,(F . b)] in F by FUNCT_1:1;

then A33: b in field R by A9;

A34: ( F . b in field S & R |_2 (R -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic ) by A9, A32;

A35: [a,b] in R by A26, XBOOLE_0:def 4;

A36: F . b in rng F by A31, FUNCT_1:def 3;

F . a in rng F by A28, FUNCT_1:def 3;

then A37: [(F . a),(F . b)] in [:(rng F),(rng F):] by A36, ZFMISC_1:87;

a in field R by A9, A29;

then A38: R -Seg a c= R -Seg b by A1, A33, A35, Th29;

A39: R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by A9, A29;

A40: now :: thesis: ( a <> b implies [(F . a),(F . b)] in S |_2 (rng F) )

( a = b implies [(F . a),(F . b)] in S |_2 (rng F) )
set P = R |_2 (R -Seg b);

A41: ( field (R |_2 (R -Seg b)) = R -Seg b & R |_2 (R -Seg b) is well-ordering ) by A1, Th25, Th32;

assume a <> b ; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)

then A42: a in R -Seg b by A35, Th1;

then (R |_2 (R -Seg b)) -Seg a = R -Seg a by A1, Th27;

then (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by A39, A38, Th22;

then [(F . a),(F . b)] in S by A2, A30, A34, A42, A41, Th51;

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

end;A41: ( field (R |_2 (R -Seg b)) = R -Seg b & R |_2 (R -Seg b) is well-ordering ) by A1, Th25, Th32;

assume a <> b ; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)

then A42: a in R -Seg b by A35, Th1;

then (R |_2 (R -Seg b)) -Seg a = R -Seg a by A1, Th27;

then (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic by A39, A38, Th22;

then [(F . a),(F . b)] in S by A2, A30, A34, A42, A41, Th51;

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

proof

hence
[(F . a),(F . b)] in S |_2 (rng F)
by A40; :: thesis: verum
assume
a = b
; :: thesis: [(F . a),(F . b)] in S |_2 (rng F)

then [(F . a),(F . b)] in S by A2, A30, Lm1;

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

end;then [(F . a),(F . b)] in S by A2, A30, Lm1;

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

A43: a in field (R |_2 (dom F)) and

A44: b in field (R |_2 (dom F)) and

A45: [(F . a),(F . b)] in S |_2 (rng F) ; :: thesis: [a,b] in R |_2 (dom F)

A46: [(F . a),(F . b)] in S by A45, XBOOLE_0:def 4;

A47: a in dom F by A43, Th12;

then A48: [a,(F . a)] in F by FUNCT_1:1;

then A49: a in field R by A9;

assume not [a,b] in R |_2 (dom F) ; :: thesis: contradiction

then A50: ( not [a,b] in R or not [a,b] in [:(dom F),(dom F):] ) by XBOOLE_0:def 4;

then A51: a <> b by A1, A47, A49, Lm1, ZFMISC_1:87;

A52: b in dom F by A44, Th12;

then A53: [b,(F . b)] in F by FUNCT_1:1;

then A54: R |_2 (R -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by A9;

A55: b in field R by A9, A53;

then A56: [b,a] in R by A1, A47, A52, A50, A49, A51, Lm4, ZFMISC_1:87;

then A57: R -Seg b c= R -Seg a by A1, A49, A55, Th29;

A58: b in R -Seg a by A47, A52, A50, A56, Th1, ZFMISC_1:87;

then (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, Th27;

then A59: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),S |_2 (S -Seg (F . b)) are_isomorphic by A54, A57, Th22;

A60: F . b in field S by A9, A53;

( F . a in field S & R |_2 (R -Seg a),S |_2 (S -Seg (F . a)) are_isomorphic ) by A9, A48;

then [(F . b),(F . a)] in S by A2, A60, A58, A25, A59, Th51;

then F . a = F . b by A2, A46, Lm3;

hence contradiction by A18, A47, A52, A51; :: thesis: verum

A61: now :: thesis: ( ex a being object st

( a in field R & Z = R -Seg a ) implies for b being object holds

( not b in field S or not rng F = S -Seg b ) )

( a in field R & Z = R -Seg a ) implies for b being object holds

( not b in field S or not rng F = S -Seg b ) )

given a being object such that A62:
a in field R
and

A63: Z = R -Seg a ; :: thesis: for b being object holds

( not b in field S or not rng F = S -Seg b )

given b being object such that A64: b in field S and

A65: rng F = S -Seg b ; :: thesis: contradiction

R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic by A10, A17, A63, A65;

then a in Z by A3, A62, A64;

hence contradiction by A63, Th1; :: thesis: verum

end;A63: Z = R -Seg a ; :: thesis: for b being object holds

( not b in field S or not rng F = S -Seg b )

given b being object such that A64: b in field S and

A65: rng F = S -Seg b ; :: thesis: contradiction

R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic by A10, A17, A63, A65;

then a in Z by A3, A62, A64;

hence contradiction by A63, Th1; :: thesis: verum

A66: now :: thesis: for a being object st a in Z holds

for b being object st [b,a] in R holds

b in Z

A82:
R |_2 Z,S |_2 (rng F) are_isomorphic
by A10, A17;for b being object st [b,a] in R holds

b in Z

let a be object ; :: thesis: ( a in Z implies for b being object st [b,a] in R holds

b in Z )

assume A67: a in Z ; :: thesis: for b being object st [b,a] in R holds

b in Z

consider c being object such that

A68: c in field S and

A69: R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic by A3, A67;

let b be object ; :: thesis: ( [b,a] in R implies b in Z )

assume A70: [b,a] in R ; :: thesis: b in Z

A71: a in field R by A3, A67;

end;b in Z )

assume A67: a in Z ; :: thesis: for b being object st [b,a] in R holds

b in Z

consider c being object such that

A68: c in field S and

A69: R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic by A3, A67;

let b be object ; :: thesis: ( [b,a] in R implies b in Z )

assume A70: [b,a] in R ; :: thesis: b in Z

A71: a in field R by A3, A67;

now :: thesis: ( a <> b implies b in Z )

hence
b in Z
by A67; :: thesis: verumset Q = S |_2 (S -Seg c);

set P = R |_2 (R -Seg a);

R |_2 (R -Seg a) is well-ordering by A1, Th25;

then A72: canonical_isomorphism_of ((R |_2 (R -Seg a)),(S |_2 (S -Seg c))) is_isomorphism_of R |_2 (R -Seg a),S |_2 (S -Seg c) by A69, Def9;

assume a <> b ; :: thesis: b in Z

then A73: b in R -Seg a by A70, Th1;

then A74: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, Th27;

A75: b in field R by A70, RELAT_1:15;

then R -Seg b c= R -Seg a by A1, A71, A73, Th30;

then A76: (R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by Th22;

field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;

then consider d being object such that

A77: d in field (S |_2 (S -Seg c)) and

A78: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),(S |_2 (S -Seg c)) |_2 ((S |_2 (S -Seg c)) -Seg d) are_isomorphic by A1, A72, A73, Th25, Th50;

A79: S -Seg c = field (S |_2 (S -Seg c)) by A2, Th32;

then A80: (S |_2 (S -Seg c)) -Seg d = S -Seg d by A2, A77, Th27;

[d,c] in S by A77, A79, Th1;

then A81: d in field S by RELAT_1:15;

then S -Seg d c= S -Seg c by A2, A68, A77, A79, Th30;

then R |_2 (R -Seg b),S |_2 (S -Seg d) are_isomorphic by A78, A74, A80, A76, Th22;

hence b in Z by A3, A75, A81; :: thesis: verum

end;set P = R |_2 (R -Seg a);

R |_2 (R -Seg a) is well-ordering by A1, Th25;

then A72: canonical_isomorphism_of ((R |_2 (R -Seg a)),(S |_2 (S -Seg c))) is_isomorphism_of R |_2 (R -Seg a),S |_2 (S -Seg c) by A69, Def9;

assume a <> b ; :: thesis: b in Z

then A73: b in R -Seg a by A70, Th1;

then A74: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, Th27;

A75: b in field R by A70, RELAT_1:15;

then R -Seg b c= R -Seg a by A1, A71, A73, Th30;

then A76: (R |_2 (R -Seg a)) |_2 (R -Seg b) = R |_2 (R -Seg b) by Th22;

field (R |_2 (R -Seg a)) = R -Seg a by A1, Th32;

then consider d being object such that

A77: d in field (S |_2 (S -Seg c)) and

A78: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),(S |_2 (S -Seg c)) |_2 ((S |_2 (S -Seg c)) -Seg d) are_isomorphic by A1, A72, A73, Th25, Th50;

A79: S -Seg c = field (S |_2 (S -Seg c)) by A2, Th32;

then A80: (S |_2 (S -Seg c)) -Seg d = S -Seg d by A2, A77, Th27;

[d,c] in S by A77, A79, Th1;

then A81: d in field S by RELAT_1:15;

then S -Seg d c= S -Seg c by A2, A68, A77, A79, Th30;

then R |_2 (R -Seg b),S |_2 (S -Seg d) are_isomorphic by A78, A74, A80, A76, Th22;

hence b in Z by A3, A75, A81; :: thesis: verum

A83: now :: thesis: ( Z = field R & ex a being object st

( a in field S & rng F = S -Seg a ) implies ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

( a in field S & rng F = S -Seg a ) implies ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

assume A84:
Z = field R
; :: thesis: ( ex a being object st

( a in field S & rng F = S -Seg a ) implies ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

given a being object such that A85: a in field S and

A86: rng F = S -Seg a ; :: thesis: ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic )

take a = a; :: thesis: ( a in field S & R,S |_2 (S -Seg a) are_isomorphic )

thus a in field S by A85; :: thesis: R,S |_2 (S -Seg a) are_isomorphic

thus R,S |_2 (S -Seg a) are_isomorphic by A82, A84, A86, Th23; :: thesis: verum

end;( a in field S & rng F = S -Seg a ) implies ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) )

given a being object such that A85: a in field S and

A86: rng F = S -Seg a ; :: thesis: ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic )

take a = a; :: thesis: ( a in field S & R,S |_2 (S -Seg a) are_isomorphic )

thus a in field S by A85; :: thesis: R,S |_2 (S -Seg a) are_isomorphic

thus R,S |_2 (S -Seg a) are_isomorphic by A82, A84, A86, Th23; :: thesis: verum

A87: now :: thesis: for a being object st a in rng F holds

for b being object st [b,a] in S holds

b in rng F

for b being object st [b,a] in S holds

b in rng F

let a be object ; :: thesis: ( a in rng F implies for b being object st [b,a] in S holds

b in rng F )

assume A88: a in rng F ; :: thesis: for b being object st [b,a] in S holds

b in rng F

consider c being object such that

A89: ( c in dom F & a = F . c ) by A88, FUNCT_1:def 3;

A90: [c,a] in F by A89, FUNCT_1:1;

then A91: a in field S by A9;

let b be object ; :: thesis: ( [b,a] in S implies b in rng F )

assume A92: [b,a] in S ; :: thesis: b in rng F

A93: R |_2 (R -Seg c),S |_2 (S -Seg a) are_isomorphic by A9, A90;

A94: c in field R by A9, A90;

end;b in rng F )

assume A88: a in rng F ; :: thesis: for b being object st [b,a] in S holds

b in rng F

consider c being object such that

A89: ( c in dom F & a = F . c ) by A88, FUNCT_1:def 3;

A90: [c,a] in F by A89, FUNCT_1:1;

then A91: a in field S by A9;

let b be object ; :: thesis: ( [b,a] in S implies b in rng F )

assume A92: [b,a] in S ; :: thesis: b in rng F

A93: R |_2 (R -Seg c),S |_2 (S -Seg a) are_isomorphic by A9, A90;

A94: c in field R by A9, A90;

now :: thesis: ( a <> b implies b in rng F )

hence
b in rng F
by A88; :: thesis: verumset Q = S |_2 (S -Seg a);

set P = R |_2 (R -Seg c);

assume a <> b ; :: thesis: b in rng F

then A95: b in S -Seg a by A92, Th1;

then A96: (S |_2 (S -Seg a)) -Seg b = S -Seg b by A2, Th27;

A97: b in field S by A92, RELAT_1:15;

then S -Seg b c= S -Seg a by A2, A91, A95, Th30;

then A98: (S |_2 (S -Seg a)) |_2 (S -Seg b) = S |_2 (S -Seg b) by Th22;

( S |_2 (S -Seg a),R |_2 (R -Seg c) are_isomorphic & S |_2 (S -Seg a) is well-ordering ) by A2, A93, Th25, Th40;

then A99: canonical_isomorphism_of ((S |_2 (S -Seg a)),(R |_2 (R -Seg c))) is_isomorphism_of S |_2 (S -Seg a),R |_2 (R -Seg c) by Def9;

field (S |_2 (S -Seg a)) = S -Seg a by A2, Th32;

then consider d being object such that

A100: d in field (R |_2 (R -Seg c)) and

A101: (S |_2 (S -Seg a)) |_2 ((S |_2 (S -Seg a)) -Seg b),(R |_2 (R -Seg c)) |_2 ((R |_2 (R -Seg c)) -Seg d) are_isomorphic by A2, A99, A95, Th25, Th50;

A102: R -Seg c = field (R |_2 (R -Seg c)) by A1, Th32;

then A103: (R |_2 (R -Seg c)) -Seg d = R -Seg d by A1, A100, Th27;

[d,c] in R by A100, A102, Th1;

then A104: d in field R by RELAT_1:15;

then R -Seg d c= R -Seg c by A1, A94, A100, A102, Th30;

then S |_2 (S -Seg b),R |_2 (R -Seg d) are_isomorphic by A101, A96, A103, A98, Th22;

then R |_2 (R -Seg d),S |_2 (S -Seg b) are_isomorphic by Th40;

then [d,b] in F by A9, A97, A104;

then ( d in dom F & b = F . d ) by FUNCT_1:1;

hence b in rng F by FUNCT_1:def 3; :: thesis: verum

end;set P = R |_2 (R -Seg c);

assume a <> b ; :: thesis: b in rng F

then A95: b in S -Seg a by A92, Th1;

then A96: (S |_2 (S -Seg a)) -Seg b = S -Seg b by A2, Th27;

A97: b in field S by A92, RELAT_1:15;

then S -Seg b c= S -Seg a by A2, A91, A95, Th30;

then A98: (S |_2 (S -Seg a)) |_2 (S -Seg b) = S |_2 (S -Seg b) by Th22;

( S |_2 (S -Seg a),R |_2 (R -Seg c) are_isomorphic & S |_2 (S -Seg a) is well-ordering ) by A2, A93, Th25, Th40;

then A99: canonical_isomorphism_of ((S |_2 (S -Seg a)),(R |_2 (R -Seg c))) is_isomorphism_of S |_2 (S -Seg a),R |_2 (R -Seg c) by Def9;

field (S |_2 (S -Seg a)) = S -Seg a by A2, Th32;

then consider d being object such that

A100: d in field (R |_2 (R -Seg c)) and

A101: (S |_2 (S -Seg a)) |_2 ((S |_2 (S -Seg a)) -Seg b),(R |_2 (R -Seg c)) |_2 ((R |_2 (R -Seg c)) -Seg d) are_isomorphic by A2, A99, A95, Th25, Th50;

A102: R -Seg c = field (R |_2 (R -Seg c)) by A1, Th32;

then A103: (R |_2 (R -Seg c)) -Seg d = R -Seg d by A1, A100, Th27;

[d,c] in R by A100, A102, Th1;

then A104: d in field R by RELAT_1:15;

then R -Seg d c= R -Seg c by A1, A94, A100, A102, Th30;

then S |_2 (S -Seg b),R |_2 (R -Seg d) are_isomorphic by A101, A96, A103, A98, Th22;

then R |_2 (R -Seg d),S |_2 (S -Seg b) are_isomorphic by Th40;

then [d,b] in F by A9, A97, A104;

then ( d in dom F & b = F . d ) by FUNCT_1:1;

hence b in rng F by FUNCT_1:def 3; :: thesis: verum

A105: now :: thesis: ( rng F = field S & ex a being object st

( a in field R & Z = R -Seg a ) implies ex a being object st

( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )

( a in field R & Z = R -Seg a ) implies ex a being object st

( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )

assume A106:
rng F = field S
; :: thesis: ( ex a being object st

( a in field R & Z = R -Seg a ) implies ex a being object st

( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )

given a being object such that A107: a in field R and

A108: Z = R -Seg a ; :: thesis: ex a being object st

( a in field R & R |_2 (R -Seg a),S are_isomorphic )

take a = a; :: thesis: ( a in field R & R |_2 (R -Seg a),S are_isomorphic )

thus a in field R by A107; :: thesis: R |_2 (R -Seg a),S are_isomorphic

thus R |_2 (R -Seg a),S are_isomorphic by A82, A106, A108, Th23; :: thesis: verum

end;( a in field R & Z = R -Seg a ) implies ex a being object st

( a in field R & R |_2 (R -Seg a),S are_isomorphic ) )

given a being object such that A107: a in field R and

A108: Z = R -Seg a ; :: thesis: ex a being object st

( a in field R & R |_2 (R -Seg a),S are_isomorphic )

take a = a; :: thesis: ( a in field R & R |_2 (R -Seg a),S are_isomorphic )

thus a in field R by A107; :: thesis: R |_2 (R -Seg a),S are_isomorphic

thus R |_2 (R -Seg a),S are_isomorphic by A82, A106, A108, Th23; :: thesis: verum

now :: thesis: ( Z = field R & rng F = field S implies R,S are_isomorphic )

hence
( R,S are_isomorphic or ex a being object st assume A109:
( Z = field R & rng F = field S )
; :: thesis: R,S are_isomorphic

( R |_2 (field R) = R & S |_2 (field S) = S ) by Th23;

hence R,S are_isomorphic by A10, A17, A109; :: thesis: verum

end;( R |_2 (field R) = R & S |_2 (field S) = S ) by Th23;

hence R,S are_isomorphic by A10, A17, A109; :: thesis: verum

( a in field R & R |_2 (R -Seg a),S are_isomorphic ) or ex a being object st

( a in field S & R,S |_2 (S -Seg a) are_isomorphic ) ) by A1, A2, A4, A15, A66, A87, A61, A83, A105, Th28; :: thesis: verum