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 A3, A2, FUNCT_1:def 3; :: 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 A7, Th1;
then A10: c in field S by RELAT_1:15;
then A11: c = F . ((F ") . c) by A4, A5, FUNCT_1:35;
( rng (F ") = dom F & dom (F ") = rng F ) by A5, FUNCT_1:33;
then A12: (F ") . c in field R by A2, A4, A10, FUNCT_1:def 3;
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 A2, A11, A12, FUNCT_1:def 6; :: 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 A14, Th1;
then A16: [c,b] in S by A1, A15;
d <> a by A14, Th1;
then c <> b by A3, A2, A5, A13, A15;
hence c in S -Seg b by A16, Th1; :: thesis: verum

end;

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