let X be set ; :: thesis: for R being Relation st R is co-well_founded & R is irreflexive & X is finite & R is finite holds
ex n being Nat st (iter (R,n)) .: X = {}
let R be Relation; :: thesis: ( R is co-well_founded & R is irreflexive & X is finite & R is finite implies ex n being Nat st (iter (R,n)) .: X = {} )
assume that
A1: ( R is co-well_founded & R is irreflexive & X is finite ) and
A2: R is finite and
A3: for n being Nat holds (iter (R,n)) .: X <> {} ; :: thesis: contradiction
defpred S1[ object ] means for n being Nat holds Im ((iter (R,n)),$1) <> {} ;
consider x0 being set such that
A4: ( x0 in X & S1[x0] ) by A1, A3, Th19;
defpred S2[ object , object , object ] means ( S1[$2] implies ( $3 in Im (R,$2) & S1[$3] ) );
A5: for n being Nat
for x being set ex y being set st S2[n,x,y]
proof
let n be Nat; :: thesis: for x being set ex y being set st S2[n,x,y]
let x be set ; :: thesis: ex y being set st S2[n,x,y]
per cases ( not S1[x] or S1[x] ) ;
suppose A6: not S1[x] ; :: thesis: ex y being set st S2[n,x,y]
take 0 ; :: thesis: S2[n,x, 0 ]
thus S2[n,x, 0 ] by A6; :: thesis: verum
end;
suppose A7: S1[x] ; :: thesis: ex y being set st S2[n,x,y]
A8: Im (R,x) c= rng R by RELAT_1:111;
now :: thesis: for n being Nat holds (iter (R,n)) .: (Im (R,x)) <> {}
let n be Nat; :: thesis: (iter (R,n)) .: (Im (R,x)) <> {}
(iter (R,n)) .: (Im (R,x)) = (R * (iter (R,n))) .: {x} by RELAT_1:126
.= Im ((iter (R,(n + 1))),x) by FUNCT_7:69 ;
hence (iter (R,n)) .: (Im (R,x)) <> {} by A7; :: thesis: verum
end;
then consider y being set such that
A9: ( y in Im (R,x) & S1[y] ) by A2, A8, Th19;
take y ; :: thesis: S2[n,x,y]
thus S2[n,x,y] by A9; :: thesis: verum
end;
end;
end;
consider f being Function such that
A10: ( dom f = NAT & f . 0 = x0 & ( for n being Nat holds S2[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 1(A5);
 defpred S3[ Nat] means S1[f . $1];
A11: S3[ 0 ] by A4, A10;
A12: for k being Nat st S3[k] holds
S3[k + 1] by A10;
A13: for k being Nat holds S3[k] from NAT_1:sch 2(A11, A12);
 A14: rng f c= field R
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in field R )
assume z in rng f ; :: thesis: z in field R
then consider y being object such that
A15: ( y in NAT & z = f . y ) by A10, FUNCT_1:def 3;
reconsider y = y as Element of NAT by A15;
( S2[y,z,f . (y + 1)] & S3[y] ) by A10, A13, A15;
then [z,(f . (y + 1))] in R by A15, RELAT_1:169;
hence z in field R by RELAT_1:15; :: thesis: verum
end;
then consider z being object such that
A16: ( z in rng f & ( for x being object st x in rng f & z <> x holds
[z,x] nin R ) ) by A1, A10, RELAT_1:42;
consider y being object such that
A17: ( y in NAT & z = f . y ) by A10, A16, FUNCT_1:def 3;
reconsider y = y as Element of NAT by A17;
( S2[y,z,f . (y + 1)] & S3[y] & y + 1 in NAT ) by A10, A13, A17, ORDINAL1:def 12;
then A18: ( [z,(f . (y + 1))] in R & f . (y + 1) in rng f ) by A10, A17, RELAT_1:169, FUNCT_1:def 3;
then ( z = f . (y + 1) & R is_irreflexive_in field R ) by A1, A16;
hence contradiction by A14, A18; :: thesis: verum