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
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 :: 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 )
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;
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 :: 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, 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;
let a be object ; :: thesis: ( a in field R implies F . a = G . a )
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;
hence F = G by A4, A8; :: thesis: verum