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 set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) holds
for a being set 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 set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) implies for a being set 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 set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ; :: thesis: for a being set st a in field R holds
[a,(F . a)] in R
A3: R is antisymmetric by A1, Def4;
defpred S₁[ set ] means [$1,(F . $1)] in R;
consider Z being set such that
A4: for a being set holds
( a in Z iff ( a in field R & S₁[a] ) ) from XBOOLE_0:sch 1();
A5: R is transitive by A1, Def4;

now

let a be set ; :: thesis: ( a in field R & R -Seg a c= Z implies a in Z )
assume A6: a in field R ; :: thesis: ( R -Seg a c= Z implies a in Z )
assume A7: R -Seg a c= Z ; :: thesis: a in Z

A8: now

let b be set ; :: thesis: ( b in R -Seg a implies ( [b,(F . a)] in R & b <> F . a ) )
assume A9: b in R -Seg a ; :: thesis: ( [b,(F . a)] in R & b <> F . a )
then A10: [b,(F . b)] in R by A4, A7;
A11: ( [b,a] in R & b <> a ) by A9, Def1;
then A12: [(F . b),(F . a)] in R by A2;
hence [b,(F . a)] in R by A5, A10, Lm2; :: thesis: b <> F . a
F . b <> F . a by A2, A11;
hence b <> F . a by A3, A10, A12, Lm3; :: thesis: verum

end;

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

end;

then A13: field R c= Z by A1, Th41;
let a be set ; :: 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 A4, A13; :: thesis: verum