let R, S be Relation; :: thesis: for F being Function st F is_isomorphism_of R,S holds
for a being object st a in field R holds
ex b being object 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 object st a in field R holds
ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b ) )

assume A1: F is_isomorphism_of R,S ; :: thesis: for a being object st a in field R holds
ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b )

then A2: dom F = field R ;
let a be object ; :: thesis: ( a in field R implies ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b ) )

assume A3: a in field R ; :: thesis: ex b being object 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;
hence b in field S by ; :: thesis: F .: (R -Seg a) = S -Seg b
A5: F is one-to-one by A1;
A6: for c being object st c in S -Seg b holds
c in F .: (R -Seg a)
proof
let c be object ; :: 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 Th1;
A9: [c,b] in S by ;
then A10: c in field S by RELAT_1:15;
then A11: c = F . ((F ") . c) by ;
( rng (F ") = dom F & dom (F ") = rng F ) by ;
then A12: (F ") . c in field R by ;
then [((F ") . c),a] in R by A1, A3, A9, A11;
then (F ") . c in R -Seg a by A8, A11, Th1;
hence c in F .: (R -Seg a) by ; :: thesis: verum
end;
for c being object st c in F .: (R -Seg a) holds
c in S -Seg b
proof
let c be object ; :: 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 object such that
A13: d in dom F and
A14: d in R -Seg a and
A15: c = F . d by FUNCT_1:def 6;
[d,a] in R by ;
then A16: [c,b] in S by ;
d <> a by ;
then c <> b by A3, A2, A5, A13, A15;
hence c in S -Seg b by ; :: thesis: verum
end;
hence F .: (R -Seg a) = S -Seg b by ; :: thesis: verum