let x, y be set ; :: 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 Th2;
hence dom (x .--> y) = field {[x,x]} by FUNCOP_1:19; :: according to WELLORD1:def 7 :: thesis: ( rng (x .--> y) = field {[y,y]} & x .--> y is one-to-one & ( for b₁, b₂ being set 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 Th2;
hence rng (x .--> y) = field {[y,y]} by FUNCOP_1:14; :: thesis: ( x .--> y is one-to-one & ( for b₁, b₂ being set 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 set 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 set ; :: 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 ZFMISC_1:33;
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 FUNCOP_1:87;
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