let R, S be Relation; :: thesis: ( R is well-ordering implies for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds

F = G )

assume A1: R is well-ordering ; :: thesis: for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds

F = G

let F, G be Function; :: thesis: ( F is_isomorphism_of R,S & G is_isomorphism_of R,S implies F = G )

assume that

A2: F is_isomorphism_of R,S and

A3: G is_isomorphism_of R,S ; :: thesis: F = G

A4: dom F = field R by A2;

A5: S is well-ordering by A1, A2, Th44;

A6: rng F = field S by A2;

A7: G is one-to-one by A3;

A8: dom G = field R by A3;

A9: G " is_isomorphism_of S,R by A3, Th39;

then A10: G " is one-to-one ;

A11: F is one-to-one by A2;

A12: rng G = field S by A3;

A13: F " is_isomorphism_of S,R by A2, Th39;

then A14: F " is one-to-one ;

for a being object st a in field R holds

F . a = G . a

F = G )

assume A1: R is well-ordering ; :: thesis: for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds

F = G

let F, G be Function; :: thesis: ( F is_isomorphism_of R,S & G is_isomorphism_of R,S implies F = G )

assume that

A2: F is_isomorphism_of R,S and

A3: G is_isomorphism_of R,S ; :: thesis: F = G

A4: dom F = field R by A2;

A5: S is well-ordering by A1, A2, Th44;

A6: rng F = field S by A2;

A7: G is one-to-one by A3;

A8: dom G = field R by A3;

A9: G " is_isomorphism_of S,R by A3, Th39;

then A10: G " is one-to-one ;

A11: F is one-to-one by A2;

A12: rng G = field S by A3;

A13: F " is_isomorphism_of S,R by A2, Th39;

then A14: F " is one-to-one ;

for a being object st a in field R holds

F . a = G . a

proof

hence
F = G
by A4, A8; :: thesis: verum
A15:
dom (F ") = field S
by A6, A11, FUNCT_1:33;

then A16: dom ((F ") * G) = field R by A8, A12, RELAT_1:27;

then A25: dom ((G ") * F) = field R by A4, A6, RELAT_1:27;

assume A33: a in field R ; :: thesis: F . a = G . a

A34: (F ") . (G . a) = ((F ") * G) . a by A8, A33, FUNCT_1:13;

G . a in rng F by A6, A8, A12, A33, FUNCT_1:def 3;

then A35: F . ((F ") . (G . a)) = G . a by A11, FUNCT_1:35;

rng (F ") = field R by A4, A11, FUNCT_1:33;

then rng ((F ") * G) = field R by A12, A15, RELAT_1:28;

then [a,(((F ") * G) . a)] in R by A1, A33, A16, A17, Th35;

then A36: [(F . a),(G . a)] in S by A2, A34, A35;

F . a in rng G by A4, A6, A12, A33, FUNCT_1:def 3;

then A37: G . ((G ") . (F . a)) = F . a by A7, FUNCT_1:35;

A38: (G ") . (F . a) = ((G ") * F) . a by A4, A33, FUNCT_1:13;

rng (G ") = field R by A8, A7, FUNCT_1:33;

then rng ((G ") * F) = field R by A6, A24, RELAT_1:28;

then [a,(((G ") * F) . a)] in R by A1, A33, A25, A26, Th35;

then [(G . a),(F . a)] in S by A3, A38, A37;

hence F . a = G . a by A5, A36, Lm3; :: thesis: verum

end;then A16: dom ((F ") * G) = field R by A8, A12, RELAT_1:27;

A17: now :: thesis: for a, b being object st [a,b] in R & a <> b holds

( [(((F ") * G) . a),(((F ") * G) . b)] in R & ((F ") * G) . a <> ((F ") * G) . b )

A24:
dom (G ") = field S
by A12, A7, FUNCT_1:33;( [(((F ") * G) . a),(((F ") * G) . b)] in R & ((F ") * G) . a <> ((F ") * G) . b )

let a, b be object ; :: thesis: ( [a,b] in R & a <> b implies ( [(((F ") * G) . a),(((F ") * G) . b)] in R & ((F ") * G) . a <> ((F ") * G) . b ) )

assume that

A18: [a,b] in R and

A19: a <> b ; :: thesis: ( [(((F ") * G) . a),(((F ") * G) . b)] in R & ((F ") * G) . a <> ((F ") * G) . b )

A20: [(G . a),(G . b)] in S by A3, A18;

A21: b in field R by A18, RELAT_1:15;

then A22: (F ") . (G . b) = ((F ") * G) . b by A8, FUNCT_1:13;

A23: a in field R by A18, RELAT_1:15;

then (F ") . (G . a) = ((F ") * G) . a by A8, FUNCT_1:13;

hence [(((F ") * G) . a),(((F ") * G) . b)] in R by A13, A20, A22; :: thesis: ((F ") * G) . a <> ((F ") * G) . b

thus ((F ") * G) . a <> ((F ") * G) . b by A14, A7, A16, A19, A23, A21, FUNCT_1:def 4; :: thesis: verum

end;assume that

A18: [a,b] in R and

A19: a <> b ; :: thesis: ( [(((F ") * G) . a),(((F ") * G) . b)] in R & ((F ") * G) . a <> ((F ") * G) . b )

A20: [(G . a),(G . b)] in S by A3, A18;

A21: b in field R by A18, RELAT_1:15;

then A22: (F ") . (G . b) = ((F ") * G) . b by A8, FUNCT_1:13;

A23: a in field R by A18, RELAT_1:15;

then (F ") . (G . a) = ((F ") * G) . a by A8, FUNCT_1:13;

hence [(((F ") * G) . a),(((F ") * G) . b)] in R by A13, A20, A22; :: thesis: ((F ") * G) . a <> ((F ") * G) . b

thus ((F ") * G) . a <> ((F ") * G) . b by A14, A7, A16, A19, A23, A21, FUNCT_1:def 4; :: thesis: verum

then A25: dom ((G ") * F) = field R by A4, A6, RELAT_1:27;

A26: now :: thesis: for a, b being object st [a,b] in R & a <> b holds

( [(((G ") * F) . a),(((G ") * F) . b)] in R & ((G ") * F) . a <> ((G ") * F) . b )

let a be object ; :: thesis: ( a in field R implies F . a = G . a )( [(((G ") * F) . a),(((G ") * F) . b)] in R & ((G ") * F) . a <> ((G ") * F) . b )

let a, b be object ; :: thesis: ( [a,b] in R & a <> b implies ( [(((G ") * F) . a),(((G ") * F) . b)] in R & ((G ") * F) . a <> ((G ") * F) . b ) )

assume that

A27: [a,b] in R and

A28: a <> b ; :: thesis: ( [(((G ") * F) . a),(((G ") * F) . b)] in R & ((G ") * F) . a <> ((G ") * F) . b )

A29: [(F . a),(F . b)] in S by A2, A27;

A30: b in field R by A27, RELAT_1:15;

then A31: (G ") . (F . b) = ((G ") * F) . b by A4, FUNCT_1:13;

A32: a in field R by A27, RELAT_1:15;

then (G ") . (F . a) = ((G ") * F) . a by A4, FUNCT_1:13;

hence [(((G ") * F) . a),(((G ") * F) . b)] in R by A9, A29, A31; :: thesis: ((G ") * F) . a <> ((G ") * F) . b

thus ((G ") * F) . a <> ((G ") * F) . b by A11, A10, A25, A28, A32, A30, FUNCT_1:def 4; :: thesis: verum

end;assume that

A27: [a,b] in R and

A28: a <> b ; :: thesis: ( [(((G ") * F) . a),(((G ") * F) . b)] in R & ((G ") * F) . a <> ((G ") * F) . b )

A29: [(F . a),(F . b)] in S by A2, A27;

A30: b in field R by A27, RELAT_1:15;

then A31: (G ") . (F . b) = ((G ") * F) . b by A4, FUNCT_1:13;

A32: a in field R by A27, RELAT_1:15;

then (G ") . (F . a) = ((G ") * F) . a by A4, FUNCT_1:13;

hence [(((G ") * F) . a),(((G ") * F) . b)] in R by A9, A29, A31; :: thesis: ((G ") * F) . a <> ((G ") * F) . b

thus ((G ") * F) . a <> ((G ") * F) . b by A11, A10, A25, A28, A32, A30, FUNCT_1:def 4; :: thesis: verum

assume A33: a in field R ; :: thesis: F . a = G . a

A34: (F ") . (G . a) = ((F ") * G) . a by A8, A33, FUNCT_1:13;

G . a in rng F by A6, A8, A12, A33, FUNCT_1:def 3;

then A35: F . ((F ") . (G . a)) = G . a by A11, FUNCT_1:35;

rng (F ") = field R by A4, A11, FUNCT_1:33;

then rng ((F ") * G) = field R by A12, A15, RELAT_1:28;

then [a,(((F ") * G) . a)] in R by A1, A33, A16, A17, Th35;

then A36: [(F . a),(G . a)] in S by A2, A34, A35;

F . a in rng G by A4, A6, A12, A33, FUNCT_1:def 3;

then A37: G . ((G ") . (F . a)) = F . a by A7, FUNCT_1:35;

A38: (G ") . (F . a) = ((G ") * F) . a by A4, A33, FUNCT_1:13;

rng (G ") = field R by A8, A7, FUNCT_1:33;

then rng ((G ") * F) = field R by A6, A24, RELAT_1:28;

then [a,(((G ") * F) . a)] in R by A1, A33, A25, A26, Th35;

then [(G . a),(F . a)] in S by A3, A38, A37;

hence F . a = G . a by A5, A36, Lm3; :: thesis: verum