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