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 object st a in field R holds

ex b being object st

( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

let F be Function; :: thesis: ( R is well-ordering & 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 & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) )

assume that

A1: R is well-ordering and

A2: 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 & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

let a be object ; :: thesis: ( a in field R implies ex b being object st

( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) )

assume a in field R ; :: thesis: ex b being object st

( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

then consider b being object such that

A3: ( b in field S & F .: (R -Seg a) = S -Seg b ) by A2, Th49;

take b ; :: thesis: ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

R -Seg a c= field R by Th9;

hence ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A1, A2, A3, Th48; :: thesis: verum

for a being object st a in field R holds

ex b being object st

( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

let F be Function; :: thesis: ( R is well-ordering & 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 & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) )

assume that

A1: R is well-ordering and

A2: 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 & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

let a be object ; :: thesis: ( a in field R implies ex b being object st

( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) )

assume a in field R ; :: thesis: ex b being object st

( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

then consider b being object such that

A3: ( b in field S & F .: (R -Seg a) = S -Seg b ) by A2, Th49;

take b ; :: thesis: ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

R -Seg a c= field R by Th9;

hence ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A1, A2, A3, Th48; :: thesis: verum