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: ( dom F = field R & rng F = field S & F is one-to-one ) by Def7;
hence A3: dom (F " ) = field S by FUNCT_1:55; :: according to WELLORD1:def 7 :: thesis: ( rng (F " ) = field R & F " is one-to-one & ( for a, b being set holds
( [a,b] in S iff ( a in field S & b in field S & [((F " ) . a),((F " ) . b)] in R ) ) ) )
thus rng (F " ) = field R by A2, FUNCT_1:55; :: thesis: ( F " is one-to-one & ( for a, b being set 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 set holds
( [a,b] in S iff ( a in field S & b in field S & [((F " ) . a),((F " ) . b)] in R ) )
let a, b be set ; :: 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 A4: [a,b] in S ; :: thesis: ( a in field S & b in field S & [((F " ) . a),((F " ) . b)] in R )
hence A5: ( a in field S & b in field S ) by RELAT_1:30; :: thesis: [((F " ) . a),((F " ) . b)] in R
then A6: ( a = F . ((F " ) . a) & b = F . ((F " ) . b) ) by A2, FUNCT_1:57;
( dom F = rng (F " ) & (F " ) . a in rng (F " ) & (F " ) . b in rng (F " ) ) by A2, A3, A5, FUNCT_1:55, FUNCT_1:def 5;
hence [((F " ) . a),((F " ) . b)] in R by A1, A2, A4, A6, Def7; :: thesis: verum

end;

assume A7: ( a in field S & b in field S & [((F " ) . a),((F " ) . b)] in R ) ; :: thesis: [a,b] in S
then ( F . ((F " ) . a) = a & F . ((F " ) . b) = b ) by A2, FUNCT_1:57;
hence [a,b] in S by A1, A7, Def7; :: thesis: verum