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 S1[ 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 & S1[a] ) ) from
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 ;
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 ;
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 ;
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 ; :: thesis: verum