let R, S be Relation; :: thesis: for F being Function st F is_isomorphism_of R,S holds
for a being set st a in field R holds
ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )
let F be Function; :: thesis: ( F is_isomorphism_of R,S implies for a being set st a in field R holds
ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b ) )
assume A1: F is_isomorphism_of R,S ; :: thesis: for a being set st a in field R holds
ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )
then A2: dom F = field R by Def7;
let a be set ; :: thesis: ( a in field R implies ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b ) )
assume A3: a in field R ; :: thesis: ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )
take b = F . a; :: thesis: ( b in field S & F .: (R -Seg a) = S -Seg b )
A4: rng F = field S by A1, Def7;
hence b in field S by A3, A2, FUNCT_1:def 5; :: thesis: F .: (R -Seg a) = S -Seg b
A5: F is one-to-one by A1, Def7;
A6: for c being set st c in S -Seg b holds
c in F .: (R -Seg a)

proof

let c be set ; :: thesis: ( c in S -Seg b implies c in F .: (R -Seg a) )
assume A7: c in S -Seg b ; :: thesis: c in F .: (R -Seg a)
then A8: c <> b by Def1;
A9: [c,b] in S by A7, Def1;
then A10: c in field S by RELAT_1:30;
then A11: c = F . ((F " ) . c) by A4, A5, FUNCT_1:57;
( rng (F " ) = dom F & dom (F " ) = rng F ) by A5, FUNCT_1:55;
then A12: (F " ) . c in field R by A2, A4, A10, FUNCT_1:def 5;
then [((F " ) . c),a] in R by A1, A3, A9, A11, Def7;
then (F " ) . c in R -Seg a by A8, A11, Def1;
hence c in F .: (R -Seg a) by A2, A11, A12, FUNCT_1:def 12; :: thesis: verum

end;

for c being set st c in F .: (R -Seg a) holds
c in S -Seg b

proof

let c be set ; :: thesis: ( c in F .: (R -Seg a) implies c in S -Seg b )
assume c in F .: (R -Seg a) ; :: thesis: c in S -Seg b
then consider d being set such that
A13: d in dom F and
A14: d in R -Seg a and
A15: c = F . d by FUNCT_1:def 12;
[d,a] in R by A14, Def1;
then A16: [c,b] in S by A1, A15, Def7;
d <> a by A14, Def1;
then c <> b by A3, A2, A5, A13, A15, FUNCT_1:def 8;
hence c in S -Seg b by A16, Def1; :: thesis: verum

end;

hence F .: (R -Seg a) = S -Seg b by A6, TARSKI:2; :: thesis: verum