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)

c in S -Seg b

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

for c being object st c in F .: (R -Seg a) holds
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;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

c in S -Seg b

proof

hence
F .: (R -Seg a) = S -Seg b
by A6, TARSKI:2; :: thesis: verum
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;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