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 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 & 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
A2: ( b in field S & F .: (R -Seg a) = S -Seg b ) by A1, Th60;
A3: R -Seg a c= field R by Th13;
take b ; :: thesis: ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
thus ( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic ) by A1, A2, A3, Th59; :: thesis: verum