let x, y be object ; :: thesis: x .--> y is_isomorphism_of {[x,x]},{[y,y]}
set F = x .--> y;
set R = {[x,x]};
set S = {[y,y]};
A1: field {[x,x]} = {x} by RELAT_1:173;
hence dom (x .--> y) = field {[x,x]} ; :: according to WELLORD1:def 7 :: thesis: ( proj2 (x .--> y) = field {[y,y]} & x .--> y is one-to-one & ( for b₁, b₂ being object holds
( ( not [b₁,b₂] in {[x,x]} or ( b₁ in field {[x,x]} & b₂ in field {[x,x]} & [((x .--> y) . b₁),((x .--> y) . b₂)] in {[y,y]} ) ) & ( not b₁ in field {[x,x]} or not b₂ in field {[x,x]} or not [((x .--> y) . b₁),((x .--> y) . b₂)] in {[y,y]} or [b₁,b₂] in {[x,x]} ) ) ) )
field {[y,y]} = {y} by RELAT_1:173;
hence rng (x .--> y) = field {[y,y]} by RELAT_1:160; :: thesis: ( x .--> y is one-to-one & ( for b₁, b₂ being object holds
( ( not [b₁,b₂] in {[x,x]} or ( b₁ in field {[x,x]} & b₂ in field {[x,x]} & [((x .--> y) . b₁),((x .--> y) . b₂)] in {[y,y]} ) ) & ( not b₁ in field {[x,x]} or not b₂ in field {[x,x]} or not [((x .--> y) . b₁),((x .--> y) . b₂)] in {[y,y]} or [b₁,b₂] in {[x,x]} ) ) ) )
thus x .--> y is one-to-one ; :: thesis: for b₁, b₂ being object holds
( ( not [b₁,b₂] in {[x,x]} or ( b₁ in field {[x,x]} & b₂ in field {[x,x]} & [((x .--> y) . b₁),((x .--> y) . b₂)] in {[y,y]} ) ) & ( not b₁ in field {[x,x]} or not b₂ in field {[x,x]} or not [((x .--> y) . b₁),((x .--> y) . b₂)] in {[y,y]} or [b₁,b₂] in {[x,x]} ) )
let a, b be object ; :: thesis: ( ( not [a,b] in {[x,x]} or ( a in field {[x,x]} & b in field {[x,x]} & [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} ) ) & ( not a in field {[x,x]} or not b in field {[x,x]} or not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} ) )

hereby :: thesis: ( not a in field {[x,x]} or not b in field {[x,x]} or not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} )

assume [a,b] in {[x,x]} ; :: thesis: ( a in field {[x,x]} & b in field {[x,x]} & [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} )
then [a,b] = [x,x] by TARSKI:def 1;
then A2: ( a = x & b = x ) by XTUPLE_0:1;
hence ( a in field {[x,x]} & b in field {[x,x]} ) by A1, TARSKI:def 1; :: thesis: [((x .--> y) . a),((x .--> y) . b)] in {[y,y]}
(x .--> y) . x = y by Th72;
hence [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} by A2, TARSKI:def 1; :: thesis: verum

end;

assume ( a in field {[x,x]} & b in field {[x,x]} ) ; :: thesis: ( not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} )
then ( a = x & b = x ) by A1, TARSKI:def 1;
hence ( not [((x .--> y) . a),((x .--> y) . b)] in {[y,y]} or [a,b] in {[x,x]} ) by TARSKI:def 1; :: thesis: verum