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 & 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 set st a in field R holds
ex b being set 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 set st a in field R holds
ex b being set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
let a be set ; :: thesis: ( a in field R implies ex b being set 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 set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
then consider b being set such that
A3: ( b in field S & F .: (R -Seg a) = S -Seg b ) by A2, Th60;
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 Th13;
hence ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A1, A2, A3, Th59; :: thesis: verum