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_{1}[ 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_{1}[a] ) )
from XBOOLE_0:sch 1();

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

( [(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

consider Z being set such that

A3: for a being object holds

( a in Z iff ( a in field R & S

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

a in Z

then A11:
field R c= Z
by A1, Th33;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

then [a,(F . a)] in R by A1, A4, A6, Th34;

hence a in Z by A3, A4; :: thesis: verum

end;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 )

F . a in rng F
by A1, A4, FUNCT_1:def 3;( [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;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

then [a,(F . a)] in R by A1, A4, A6, Th34;

hence a in Z by A3, A4; :: thesis: verum

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