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

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 )
then A7: F . a in rng F by A1, FUNCT_1:def 5;
assume A8: R -Seg a c= Z ; :: thesis: a in Z

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 A5, A8;
( [b,a] in R & b <> a ) by A9, Def1;
then A11: ( [(F . b),(F . a)] in R & F . b <> F . a ) by A2;
hence [b,(F . a)] in R by A3, A10, Lm2; :: thesis: b <> F . a
thus b <> F . a by A4, A10, A11, Lm3; :: thesis: verum

end;

then [a,(F . a)] in R by A1, A6, A7, Th42;
hence a in Z by A5, A6; :: thesis: verum

end;

then A12: 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 A5, A12; :: thesis: verum