let R, S be Relation; :: thesis: for F being Function st R is well-ordering & 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: ( R is well-ordering & 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: ( R is well-ordering & 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 )
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 A2: a in field R ; :: thesis: ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )
A3: ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) by A1, Def7;
take b = F . a; :: thesis: ( b in field S & F .: (R -Seg a) = S -Seg b )
thus b in field S by A2, A3, FUNCT_1:def 5; :: thesis: F .: (R -Seg a) = S -Seg b
A4: 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
A5: ( d in dom F & d in R -Seg a & c = F . d ) by FUNCT_1:def 12;
A6: ( [d,a] in R & d <> a ) by A5, Def1;
then A7: [c,b] in S by A1, A5, Def7;
c <> b by A2, A3, A5, A6, FUNCT_1:def 8;
hence c in S -Seg b by A7, Def1; :: thesis: verum

end;

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 c in S -Seg b ; :: thesis: c in F .: (R -Seg a)
then A8: ( [c,b] in S & c <> b ) by Def1;
then A9: c in field S by RELAT_1:30;
then A10: c = F . ((F " ) . c) by A3, FUNCT_1:57;
( rng (F " ) = dom F & dom (F " ) = rng F ) by A3, FUNCT_1:55;
then A11: (F " ) . c in field R by A3, A9, FUNCT_1:def 5;
then [((F " ) . c),a] in R by A1, A2, A8, A10, Def7;
then (F " ) . c in R -Seg a by A8, A10, Def1;
hence c in F .: (R -Seg a) by A3, A10, A11, FUNCT_1:def 12; :: thesis: verum

end;

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