let R, S be Relation; :: thesis: for F being Function st F is_isomorphism_of R,S holds

F " is_isomorphism_of S,R

let F be Function; :: thesis: ( F is_isomorphism_of R,S implies F " is_isomorphism_of S,R )

assume A1: F is_isomorphism_of R,S ; :: thesis: 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; :: according to WELLORD1:def 7 :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( [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 ) ) :: thesis: ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R implies [a,b] in S )

A9: ( a in field S & b in field S ) and

A10: [((F ") . a),((F ") . b)] in R ; :: thesis: [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; :: thesis: verum

F " is_isomorphism_of S,R

let F be Function; :: thesis: ( F is_isomorphism_of R,S implies F " is_isomorphism_of S,R )

assume A1: F is_isomorphism_of R,S ; :: thesis: 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; :: according to WELLORD1:def 7 :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( [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 ) ) :: thesis: ( a in field S & b in field S & [((F ") . a),((F ") . b)] in R implies [a,b] in S )

proof

assume that
A5:
dom F = rng (F ")
by A2, FUNCT_1:33;

assume A6: [a,b] in S ; :: thesis: ( 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; :: thesis: [((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; :: thesis: verum

end;assume A6: [a,b] in S ; :: thesis: ( 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; :: thesis: [((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; :: thesis: verum

A9: ( a in field S & b in field S ) and

A10: [((F ") . a),((F ") . b)] in R ; :: thesis: [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; :: thesis: verum