let R be Relation; :: thesis: for F being Function st R is well-ordering & dom F = field R & rng F c= field R & ( for a, b being object st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) holds
for a being object st a in field R holds
[a,(F . a)] in R
let F be Function; :: thesis: ( R is well-ordering & dom F = field R & rng F c= field R & ( for a, b being object st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) implies for a being object st a in field R holds
[a,(F . a)] in R )
assume that
A1: ( R is well-ordering & dom F = field R & rng F c= field R ) and
A2: for a, b being object st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ; :: thesis: for a being object st a in field R holds
[a,(F . a)] in R
defpred S₁[ object ] means [$1,(F . $1)] in R;
consider Z being set such that
A3: for a being object holds
( a in Z iff ( a in field R & S₁[a] ) ) from XBOOLE_0:sch 1();

now :: thesis: for a being object st a in field R & R -Seg a c= Z holds
a in Z

let a be object ; :: thesis: ( a in field R & R -Seg a c= Z implies a in Z )
assume A4: a in field R ; :: thesis: ( R -Seg a c= Z implies a in Z )
assume A5: R -Seg a c= Z ; :: thesis: a in Z

A6: now :: thesis: for b being object st b in R -Seg a holds
( [b,(F . a)] in R & b <> F . a )

let b be object ; :: thesis: ( b in R -Seg a implies ( [b,(F . a)] in R & b <> F . a ) )
assume A7: b in R -Seg a ; :: thesis: ( [b,(F . a)] in R & b <> F . a )
then A8: [b,(F . b)] in R by A3, A5;
A9: ( [b,a] in R & b <> a ) by A7, Th1;
then A10: [(F . b),(F . a)] in R by A2;
hence [b,(F . a)] in R by A1, A8, Lm2; :: thesis: b <> F . a
F . b <> F . a by A2, A9;
hence b <> F . a by A1, A8, A10, Lm3; :: thesis: verum

end;

F . a in rng F by A1, A4, FUNCT_1:def 3;
then [a,(F . a)] in R by A1, A4, A6, Th34;
hence a in Z by A3, A4; :: thesis: verum

end;

then A11: field R c= Z by A1, Th33;
let a be object ; :: thesis: ( a in field R implies [a,(F . a)] in R )
assume a in field R ; :: thesis: [a,(F . a)] in R
hence [a,(F . a)] in R by A3, A11; :: thesis: verum