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 A2: ( F is_isomorphism_of R,S & G is_isomorphism_of R,S ) ; :: thesis: F = G
then S is well-ordering by A1, Th54;
then A3: S is antisymmetric by Def4;
A4: ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) by A2, Def7;
A5: F " is_isomorphism_of S,R by A2, Th49;
then A6: ( F " is one-to-one & ( for a, b being set holds
( [a,b] in S iff ( a in field S & b in field S & [((F " ) . a),((F " ) . b)] in R ) ) ) ) by Def7;
A7: ( dom G = field R & rng G = field S & G is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(G . a),(G . b)] in S ) ) ) ) by A2, Def7;
A8: G " is_isomorphism_of S,R by A2, Th49;
then A9: ( G " is one-to-one & ( for a, b being set holds
( [a,b] in S iff ( a in field S & b in field S & [((G " ) . a),((G " ) . b)] in R ) ) ) ) by Def7;
for a being set st a in field R holds
F . a = G . a

proof

let a be set ; :: thesis: ( a in field R implies F . a = G . a )
assume A10: a in field R ; :: thesis: F . a = G . a
A11: ( dom (G " ) = field S & dom (F " ) = field S & rng (G " ) = field R & rng (F " ) = field R ) by A4, A7, FUNCT_1:55;
then A12: ( dom ((G " ) * F) = field R & dom ((F " ) * G) = field R ) by A4, A7, RELAT_1:46;
A13: ( rng ((G " ) * F) = field R & rng ((F " ) * G) = field R ) by A4, A7, A11, RELAT_1:47;

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 A14: ( [a,b] in R & a <> b ) ; :: thesis: ( [(((G " ) * F) . a),(((G " ) * F) . b)] in R & ((G " ) * F) . a <> ((G " ) * F) . b )
then A15: [(F . a),(F . b)] in S by A2, Def7;
A16: ( a in field R & b in field R ) by A14, RELAT_1:30;
then ( (G " ) . (F . a) = ((G " ) * F) . a & (G " ) . (F . b) = ((G " ) * F) . b ) by A4, FUNCT_1:23;
hence [(((G " ) * F) . a),(((G " ) * F) . b)] in R by A8, A15, Def7; :: thesis: ((G " ) * F) . a <> ((G " ) * F) . b
(G " ) * F is one-to-one by A4, A9;
hence ((G " ) * F) . a <> ((G " ) * F) . b by A12, A14, A16, FUNCT_1:def 8; :: thesis: verum

end;

then A17: [a,(((G " ) * F) . a)] in R by A1, A10, A12, A13, Th43;
A18: (G " ) . (F . a) = ((G " ) * F) . a by A4, A10, FUNCT_1:23;
F . a in rng G by A4, A7, A10, FUNCT_1:def 5;
then G . ((G " ) . (F . a)) = F . a by A7, FUNCT_1:57;
then A19: [(G . a),(F . a)] in S by A2, A17, A18, Def7;

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 A20: ( [a,b] in R & a <> b ) ; :: thesis: ( [(((F " ) * G) . a),(((F " ) * G) . b)] in R & ((F " ) * G) . a <> ((F " ) * G) . b )
then A21: [(G . a),(G . b)] in S by A2, Def7;
A22: ( a in field R & b in field R ) by A20, RELAT_1:30;
then ( (F " ) . (G . a) = ((F " ) * G) . a & (F " ) . (G . b) = ((F " ) * G) . b ) by A7, FUNCT_1:23;
hence [(((F " ) * G) . a),(((F " ) * G) . b)] in R by A5, A21, Def7; :: thesis: ((F " ) * G) . a <> ((F " ) * G) . b
(F " ) * G is one-to-one by A6, A7;
hence ((F " ) * G) . a <> ((F " ) * G) . b by A12, A20, A22, FUNCT_1:def 8; :: thesis: verum

end;

then A23: [a,(((F " ) * G) . a)] in R by A1, A10, A12, A13, Th43;
A24: (F " ) . (G . a) = ((F " ) * G) . a by A7, A10, FUNCT_1:23;
G . a in rng F by A4, A7, A10, FUNCT_1:def 5;
then F . ((F " ) . (G . a)) = G . a by A4, FUNCT_1:57;
then [(F . a),(G . a)] in S by A2, A23, A24, Def7;
hence F . a = G . a by A3, A19, Lm3; :: thesis: verum

end;

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