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, Def7;
S is well-ordering by A1, A2, Th54;
then A5: S is antisymmetric by Def4;
A6: rng F = field S by A2, Def7;
A7: G is one-to-one by A3, Def7;
A8: dom G = field R by A3, Def7;
A9: G " is_isomorphism_of S,R by A3, Th49;
then A10: G " is one-to-one by Def7;
A11: F is one-to-one by A2, Def7;
A12: rng G = field S by A3, Def7;
A13: F " is_isomorphism_of S,R by A2, Th49;
then A14: F " is one-to-one by Def7;
for a being set st a in field R holds
F . a = G . a

proof

A15: dom (F " ) = field S by A6, A11, FUNCT_1:55;
then A16: dom ((F " ) * G) = field R by A8, A12, RELAT_1:46;

A17: now

let a, b be set ; :: 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, Def7;
A21: b in field R by A18, RELAT_1:30;
then A22: (F " ) . (G . b) = ((F " ) * G) . b by A8, FUNCT_1:23;
A23: a in field R by A18, RELAT_1:30;
then (F " ) . (G . a) = ((F " ) * G) . a by A8, FUNCT_1:23;
hence [(((F " ) * G) . a),(((F " ) * G) . b)] in R by A13, A20, A22, Def7; :: thesis: ((F " ) * G) . a <> ((F " ) * G) . b
thus ((F " ) * G) . a <> ((F " ) * G) . b by A14, A7, A16, A19, A23, A21, FUNCT_1:def 8; :: thesis: verum

end;

A24: dom (G " ) = field S by A12, A7, FUNCT_1:55;
then A25: dom ((G " ) * F) = field R by A4, A6, RELAT_1:46;

A26: now

let a, b be set ; :: 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, Def7;
A30: b in field R by A27, RELAT_1:30;
then A31: (G " ) . (F . b) = ((G " ) * F) . b by A4, FUNCT_1:23;
A32: a in field R by A27, RELAT_1:30;
then (G " ) . (F . a) = ((G " ) * F) . a by A4, FUNCT_1:23;
hence [(((G " ) * F) . a),(((G " ) * F) . b)] in R by A9, A29, A31, Def7; :: thesis: ((G " ) * F) . a <> ((G " ) * F) . b
thus ((G " ) * F) . a <> ((G " ) * F) . b by A11, A10, A25, A28, A32, A30, FUNCT_1:def 8; :: thesis: verum

end;

let a be set ; :: 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:23;
G . a in rng F by A6, A8, A12, A33, FUNCT_1:def 5;
then A35: F . ((F " ) . (G . a)) = G . a by A11, FUNCT_1:57;
rng (F " ) = field R by A4, A11, FUNCT_1:55;
then rng ((F " ) * G) = field R by A12, A15, RELAT_1:47;
then [a,(((F " ) * G) . a)] in R by A1, A33, A16, A17, Th43;
then A36: [(F . a),(G . a)] in S by A2, A34, A35, Def7;
F . a in rng G by A4, A6, A12, A33, FUNCT_1:def 5;
then A37: G . ((G " ) . (F . a)) = F . a by A7, FUNCT_1:57;
A38: (G " ) . (F . a) = ((G " ) * F) . a by A4, A33, FUNCT_1:23;
rng (G " ) = field R by A8, A7, FUNCT_1:55;
then rng ((G " ) * F) = field R by A6, A24, RELAT_1:47;
then [a,(((G " ) * F) . a)] in R by A1, A33, A25, A26, Th43;
then [(G . a),(F . a)] in S by A3, A38, A37, Def7;
hence F . a = G . a by A5, A36, Lm3; :: thesis: verum

end;

hence F = G by A4, A8, FUNCT_1:9; :: thesis: verum