let R, S be Relation; for F being Function st F is_isomorphism_of R,S holds
F " is_isomorphism_of S,R
let F be Function; ( F is_isomorphism_of R,S implies F " is_isomorphism_of S,R )
assume A1:
F is_isomorphism_of R,S
; F " is_isomorphism_of S,R
then A2:
F is one-to-one
;
A3:
rng F = field S
by A1;
hence A4:
dom (F ") = field S
by A2, FUNCT_1:33; WELLORD1:def 7 ( rng (F ") = field R & F " is one-to-one & ( for a, b being object holds
( [a,b] in S iff ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) ) ) )
dom F = field R
by A1;
hence
rng (F ") = field R
by A2, FUNCT_1:33; ( F " is one-to-one & ( for a, b being object holds
( [a,b] in S iff ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) ) ) )
thus
F " is one-to-one
by A2; for a, b being object holds
( [a,b] in S iff ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) )
let a, b be object ; ( [a,b] in S iff ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) )
thus
( [a,b] in S implies ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R ) )
( a in field S & b in field S & [((F ") . a),((F ") . b)] in R implies [a,b] in S )proof
A5:
dom F = rng (F ")
by A2, FUNCT_1:33;
assume A6:
[a,b] in S
;
( a in field S & b in field S & [((F ") . a),((F ") . b)] in R )
hence A7:
(
a in field S &
b in field S )
by RELAT_1:15;
[((F ") . a),((F ") . b)] in R
then A8:
(
(F ") . a in rng (F ") &
(F ") . b in rng (F ") )
by A4, FUNCT_1:def 3;
(
a = F . ((F ") . a) &
b = F . ((F ") . b) )
by A3, A2, A7, FUNCT_1:35;
hence
[((F ") . a),((F ") . b)] in R
by A1, A6, A5, A8;
verum
end;
assume that
A9:
( a in field S & b in field S )
and
A10:
[((F ") . a),((F ") . b)] in R
; [a,b] in S
( F . ((F ") . a) = a & F . ((F ") . b) = b )
by A3, A2, A9, FUNCT_1:35;
hence
[a,b] in S
by A1, A10; verum