let R, S be Relation; ( 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
; 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; ( 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
; 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
A15:
dom (F ") = field S
by A6, A11, FUNCT_1:33;
then A16:
dom ((F ") * G) = field R
by A8, A12, RELAT_1:27;
A17:
now 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 )let a,
b be
object ;
( [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
;
( [(((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;
((F ") * G) . a <> ((F ") * G) . bthus
((F ") * G) . a <> ((F ") * G) . b
by A14, A7, A16, A19, A23, A21, FUNCT_1:def 4;
verum end;
A24:
dom (G ") = field S
by A12, A7, FUNCT_1:33;
then A25:
dom ((G ") * F) = field R
by A4, A6, RELAT_1:27;
A26:
now 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,
b be
object ;
( [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
;
( [(((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;
((G ") * F) . a <> ((G ") * F) . bthus
((G ") * F) . a <> ((G ") * F) . b
by A11, A10, A25, A28, A32, A30, FUNCT_1:def 4;
verum end;
let a be
object ;
( a in field R implies F . a = G . a )
assume A33:
a in field R
;
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;
verum
end;
hence
F = G
by A4, A8; verum