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 ;
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 ;
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 ;
then A16: dom ((F ") * G) = field R by ;
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 ;
A21: b in field R by ;
then A22: (F ") . (G . b) = ((F ") * G) . b by ;
A23: a in field R by ;
then (F ") . (G . a) = ((F ") * G) . a by ;
hence [(((F ") * G) . a),(((F ") * G) . b)] in R by ; :: thesis: ((F ") * G) . a <> ((F ") * G) . b
thus ((F ") * G) . a <> ((F ") * G) . b by ; :: thesis: verum
end;
A24: dom (G ") = field S by ;
then A25: dom ((G ") * F) = field R by ;
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 ;
A30: b in field R by ;
then A31: (G ") . (F . b) = ((G ") * F) . b by ;
A32: a in field R by ;
then (G ") . (F . a) = ((G ") * F) . a by ;
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 ; :: 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 ;
G . a in rng F by ;
then A35: F . ((F ") . (G . a)) = G . a by ;
rng (F ") = field R by ;
then rng ((F ") * G) = field R by ;
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 ;
then A37: G . ((G ") . (F . a)) = F . a by ;
A38: (G ") . (F . a) = ((G ") * F) . a by ;
rng (G ") = field R by ;
then rng ((G ") * F) = field R by ;
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