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_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in {[x,x]} or ( b_{1} in field {[x,x]} & b_{2} in field {[x,x]} & [((x .--> y) . b_{1}),((x .--> y) . b_{2})] in {[y,y]} ) ) & ( not b_{1} in field {[x,x]} or not b_{2} in field {[x,x]} or not [((x .--> y) . b_{1}),((x .--> y) . b_{2})] in {[y,y]} or [b_{1},b_{2}] 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_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in {[x,x]} or ( b_{1} in field {[x,x]} & b_{2} in field {[x,x]} & [((x .--> y) . b_{1}),((x .--> y) . b_{2})] in {[y,y]} ) ) & ( not b_{1} in field {[x,x]} or not b_{2} in field {[x,x]} or not [((x .--> y) . b_{1}),((x .--> y) . b_{2})] in {[y,y]} or [b_{1},b_{2}] in {[x,x]} ) ) ) )

thus x .--> y is one-to-one ; :: thesis: for b_{1}, b_{2} being object holds

( ( not [b_{1},b_{2}] in {[x,x]} or ( b_{1} in field {[x,x]} & b_{2} in field {[x,x]} & [((x .--> y) . b_{1}),((x .--> y) . b_{2})] in {[y,y]} ) ) & ( not b_{1} in field {[x,x]} or not b_{2} in field {[x,x]} or not [((x .--> y) . b_{1}),((x .--> y) . b_{2})] in {[y,y]} or [b_{1},b_{2}] 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]} ) )

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

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

( ( not [b

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

( ( not [b

thus x .--> y is one-to-one ; :: thesis: for b

( ( not [b

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 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]} )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;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

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