let R, S be Relation; 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; ( 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
; 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 ; ( 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
; 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
; ( 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; verum