let R be non empty RelStr ; :: thesis: ( R is well_founded iff for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H )

set c = the carrier of R;
set r = the InternalRel of R;
defpred S1[] means for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H;
reconsider ac = omega +` (card the carrier of R) as infinite Cardinal ;
set V = nextcard ac;
deffunc H1( Element of the carrier of R, Element of PFuncs ( the carrier of R,(nextcard ac))) -> set = sup (rng \$2);
A1: for x being Element of the carrier of R
for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H1(x,p) in nextcard ac
proof
let x be Element of the carrier of R; :: thesis: for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H1(x,p) in nextcard ac
let p be Element of PFuncs ( the carrier of R,(nextcard ac)); :: thesis: H1(x,p) in nextcard ac
( card (dom p) c= card the carrier of R & card (rng p) c= card (dom p) ) by ;
then A2: card (rng p) c= card the carrier of R ;
card the carrier of R c= ac by CARD_2:94;
then card (rng p) c= ac by A2;
then A3: card (rng p) in nextcard ac by ;
nextcard ac is regular by CARD_5:30;
hence H1(x,p) in nextcard ac by ; :: thesis: verum
end;
consider H being Function of [: the carrier of R,(PFuncs ( the carrier of R,(nextcard ac))):],(nextcard ac) such that
A4: for x being Element of the carrier of R
for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H . (x,p) = H1(x,p) from thus ( R is well_founded implies S1[] ) :: thesis: ( ( for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H ) implies R is well_founded )
proof
assume A5: R is well_founded ; :: thesis: S1[]
let V be non empty set ; :: thesis: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V ex F being Function of the carrier of R,V st F is_recursively_expressed_by H
let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V; :: thesis: ex F being Function of the carrier of R,V st F is_recursively_expressed_by H
defpred S2[ PartFunc of the carrier of R,V] means ( dom \$1 is lower & ( for x being set st x in dom \$1 holds
\$1 . x = H . [x,(\$1 | ( the InternalRel of R -Seg x))] ) );
consider fs being Subset of (PFuncs ( the carrier of R,V)) such that
A6: for f being PartFunc of the carrier of R,V holds
( f in fs iff S2[f] ) from
now :: thesis: for f, g being Function st f in fs & g in fs holds
f tolerates g
let f, g be Function; :: thesis: ( f in fs & g in fs implies f tolerates g )
assume that
A7: f in fs and
A8: g in fs ; :: thesis:
reconsider ff = f, gg = g as PartFunc of the carrier of R,V by ;
defpred S3[ set ] means ( \$1 in dom ff & \$1 in dom gg & ff . \$1 <> gg . \$1 );
assume not f tolerates g ; :: thesis: contradiction
then consider x being object such that
A9: x in (dom ff) /\ (dom gg) and
A10: ff . x <> gg . x by PARTFUN1:def 4;
reconsider x = x as Element of R by A9;
A11: S3[x] by A9, A10, XBOOLE_0:def 4;
consider x0 being Element of R such that
A12: S3[x0] and
A13: for y being Element of R holds
( not x0 <> y or not S3[y] or not [y,x0] in the InternalRel of R ) from ff | ( the InternalRel of R -Seg x0) = gg | ( the InternalRel of R -Seg x0)
proof
set fr = ff | ( the InternalRel of R -Seg x0);
set gr = gg | ( the InternalRel of R -Seg x0);
assume A14: not ff | ( the InternalRel of R -Seg x0) = gg | ( the InternalRel of R -Seg x0) ; :: thesis: contradiction
A15: dom ff is lower by A6, A7;
then A16: dom (ff | ( the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 by ;
A17: dom gg is lower by A6, A8;
then dom (ff | ( the InternalRel of R -Seg x0)) = dom (gg | ( the InternalRel of R -Seg x0)) by ;
then consider x1 being object such that
A18: x1 in dom (ff | ( the InternalRel of R -Seg x0)) and
A19: (ff | ( the InternalRel of R -Seg x0)) . x1 <> (gg | ( the InternalRel of R -Seg x0)) . x1 by A14;
A20: [x1,x0] in the InternalRel of R by ;
reconsider x1 = x1 as Element of R by A18;
A21: ( (ff | ( the InternalRel of R -Seg x0)) . x1 = ff . x1 & (gg | ( the InternalRel of R -Seg x0)) . x1 = gg . x1 ) by ;
A22: x1 <> x0 by ;
A23: x1 in dom gg by ;
x1 in dom ff by ;
hence contradiction by A13, A19, A20, A21, A22, A23; :: thesis: verum
end;
then ff . x0 = H . [x0,(gg | ( the InternalRel of R -Seg x0))] by A6, A7, A12
.= gg . x0 by A6, A8, A12 ;
hence contradiction by A12; :: thesis: verum
end;
then reconsider ufs = union fs as Function by Th1;
A24: now :: thesis: for x being set st x in dom ufs holds
ufs . x = H . [x,(ufs | ( the InternalRel of R -Seg x))]
let x be set ; :: thesis: ( x in dom ufs implies ufs . x = H . [x,(ufs | ( the InternalRel of R -Seg x))] )
assume x in dom ufs ; :: thesis: ufs . x = H . [x,(ufs | ( the InternalRel of R -Seg x))]
then [x,(ufs . x)] in ufs by FUNCT_1:1;
then consider fx being set such that
A25: [x,(ufs . x)] in fx and
A26: fx in fs by TARSKI:def 4;
reconsider ff = fx as PartFunc of the carrier of R,V by ;
A27: x in dom ff by ;
A28: ( dom ff is lower & ff c= ufs ) by ;
thus ufs . x = ff . x by
.= H . [x,(ff | ( the InternalRel of R -Seg x))] by A6, A26, A27
.= H . [x,(ufs | ( the InternalRel of R -Seg x))] by ; :: thesis: verum
end;
A29: dom ufs c= the carrier of R
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in dom ufs or y in the carrier of R )
assume y in dom ufs ; :: thesis: y in the carrier of R
then [y,(ufs . y)] in ufs by FUNCT_1:1;
then consider fx being set such that
A30: [y,(ufs . y)] in fx and
A31: fx in fs by TARSKI:def 4;
consider ff being Function such that
A32: ff = fx and
A33: dom ff c= the carrier of R and
rng ff c= V by ;
y in dom ff by ;
hence y in the carrier of R by A33; :: thesis: verum
end;
A34: rng ufs c= V
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ufs or y in V )
assume y in rng ufs ; :: thesis: y in V
then consider x being object such that
A35: ( x in dom ufs & y = ufs . x ) by FUNCT_1:def 3;
[x,y] in ufs by ;
then consider fx being set such that
A36: [x,y] in fx and
A37: fx in fs by TARSKI:def 4;
consider ff being Function such that
A38: ff = fx and
dom ff c= the carrier of R and
A39: rng ff c= V by ;
y in rng ff by ;
hence y in V by A39; :: thesis: verum
end;
A40: now :: thesis: for x, y being object st x in dom ufs & [y,x] in the InternalRel of R holds
y in dom ufs
let x, y be object ; :: thesis: ( x in dom ufs & [y,x] in the InternalRel of R implies y in dom ufs )
assume that
A41: x in dom ufs and
A42: [y,x] in the InternalRel of R ; :: thesis: y in dom ufs
[x,(ufs . x)] in ufs by ;
then consider fx being set such that
A43: [x,(ufs . x)] in fx and
A44: fx in fs by TARSKI:def 4;
reconsider ff = fx as PartFunc of the carrier of R,V by ;
ff c= ufs by ;
then A45: dom ff c= dom ufs by GRFUNC_1:2;
( dom ff is lower & x in dom ff ) by ;
then y in dom ff by A42;
hence y in dom ufs by A45; :: thesis: verum
end;
A46: dom ufs = the carrier of R
proof
defpred S3[ set ] means ( \$1 in the carrier of R & not \$1 in dom ufs );
assume dom ufs <> the carrier of R ; :: thesis: contradiction
then consider x being object such that
A47: ( ( x in dom ufs & not x in the carrier of R ) or ( x in the carrier of R & not x in dom ufs ) ) by TARSKI:2;
reconsider x = x as Element of R by ;
A48: S3[x] by A47;
consider x0 being Element of R such that
A49: S3[x0] and
A50: for y being Element of R holds
( not x0 <> y or not S3[y] or not [y,x0] in the InternalRel of R ) from set nv = x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]);
set nf = ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]));
A51: dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) = {x0} ;
A52: rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= V
proof
ufs in PFuncs ( the carrier of R,V) by ;
then ufs is PartFunc of the carrier of R,V by PARTFUN1:46;
then ufs | ( the InternalRel of R -Seg x0) is PartFunc of the carrier of R,V by PARTFUN1:11;
then A53: ufs | ( the InternalRel of R -Seg x0) in PFuncs ( the carrier of R,V) by PARTFUN1:45;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) or x in V )
assume A54: x in rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) ; :: thesis: x in V
assume A55: not x in V ; :: thesis: contradiction
then ( rng (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= (rng ufs) \/ (rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) & not x in rng ufs ) by ;
then A56: x in rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by ;
rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) = {(H . [x0,(ufs | ( the InternalRel of R -Seg x0))])} by FUNCOP_1:8;
then x = H . (x0,(ufs | ( the InternalRel of R -Seg x0))) by ;
hence contradiction by A55, A53, BINOP_1:17; :: thesis: verum
end;
A57: dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) = (dom ufs) \/ (dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) by FUNCT_4:def 1;
dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= the carrier of R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) or x in the carrier of R )
assume that
A58: x in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) and
A59: not x in the carrier of R ; :: thesis: contradiction
not x in dom ufs by ;
then x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by ;
hence contradiction by A51, A59; :: thesis: verum
end;
then A60: ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) in PFuncs ( the carrier of R,V) by ;
x0 in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by TARSKI:def 1;
then x0 in dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) by ;
then A61: [x0,((ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) . x0)] in ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by FUNCT_1:1;
reconsider nf = ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) as PartFunc of the carrier of R,V by ;
A62: now :: thesis: for x being set st x in dom nf holds
nf . x = H . [x,(nf | ( the InternalRel of R -Seg x))]
let x be set ; :: thesis: ( x in dom nf implies nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))] )
assume A63: x in dom nf ; :: thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))]
per cases ( x in dom ufs or x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) ) by ;
suppose A64: x in dom ufs ; :: thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))]
A65: {x0} misses the InternalRel of R -Seg x
proof
assume {x0} meets the InternalRel of R -Seg x ; :: thesis: contradiction
then consider y being object such that
A66: y in {x0} and
A67: y in the InternalRel of R -Seg x by XBOOLE_0:3;
y = x0 by ;
then [x0,x] in the InternalRel of R by ;
hence contradiction by A40, A49, A64; :: thesis: verum
end;
not x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by ;
hence nf . x = ufs . x by FUNCT_4:11
.= H . [x,(ufs | ( the InternalRel of R -Seg x))] by
.= H . [x,(nf | ( the InternalRel of R -Seg x))] by ;
:: thesis: verum
end;
suppose A68: x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) ; :: thesis: nf . b1 = H . [b1,(nf | ( the InternalRel of R -Seg b1))]
A69: {x0} misses the InternalRel of R -Seg x0
proof
assume {x0} meets the InternalRel of R -Seg x0 ; :: thesis: contradiction
then consider x being object such that
A70: x in {x0} and
A71: x in the InternalRel of R -Seg x0 by XBOOLE_0:3;
x = x0 by ;
hence contradiction by A71, WELLORD1:1; :: thesis: verum
end;
A72: x = x0 by ;
hence nf . x = (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) . x0 by
.= H . [x0,(ufs | ( the InternalRel of R -Seg x0))] by FUNCOP_1:72
.= H . [x,(nf | ( the InternalRel of R -Seg x))] by ;
:: thesis: verum
end;
end;
end;
dom nf is lower
proof
let x, y be object ; :: according to WELLFND1:def 1 :: thesis: ( x in dom nf & [y,x] in the InternalRel of R implies y in dom nf )
assume that
A73: x in dom nf and
A74: [y,x] in the InternalRel of R ; :: thesis: y in dom nf
assume A75: not y in dom nf ; :: thesis: contradiction
then A76: not y in dom ufs by ;
then not x in dom ufs by ;
then x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by ;
then A77: x = x0 by TARSKI:def 1;
reconsider y = y as Element of R by ;
not y in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by ;
then y <> x0 by TARSKI:def 1;
hence contradiction by A50, A74, A76, A77; :: thesis: verum
end;
then nf in fs by ;
then [x0,(nf . x0)] in ufs by ;
hence contradiction by A49, FUNCT_1:1; :: thesis: verum
end;
then reconsider ufs = ufs as Function of the carrier of R,V by ;
take ufs ; :: thesis:
let x be Element of the carrier of R; :: according to WELLFND1:def 5 :: thesis: ufs . x = H . (x,(ufs | ( the InternalRel of R -Seg x)))
thus ufs . x = H . (x,(ufs | ( the InternalRel of R -Seg x))) by ; :: thesis: verum
end;
assume S1[] ; :: thesis: R is well_founded
then consider rk being Function of the carrier of R,(nextcard ac) such that
A78: rk is_recursively_expressed_by H ;
let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 2 :: thesis: ( not Y c= the carrier of R or Y = {} or ex b1 being object st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )

assume that
A79: Y c= the carrier of R and
A80: Y <> {} ; :: thesis: ex b1 being object st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )

set m = inf (rk .: Y);
consider b being object such that
A81: b in Y by ;
A82: dom rk = the carrier of R by FUNCT_2:def 1;
then rk . b in rk .: Y by ;
then inf (rk .: Y) in rk .: Y by ORDINAL2:17;
then consider a being object such that
A83: a in dom rk and
A84: a in Y and
A85: rk . a = inf (rk .: Y) by FUNCT_1:def 6;
reconsider a = a as set by TARSKI:1;
take a ; :: thesis: ( a in Y & the InternalRel of R -Seg a misses Y )
thus a in Y by A84; :: thesis: the InternalRel of R -Seg a misses Y
assume ( the InternalRel of R -Seg a) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then consider e being object such that
A86: e in ( the InternalRel of R -Seg a) /\ Y by XBOOLE_0:def 1;
A87: e in the InternalRel of R -Seg a by ;
reconsider a = a as Element of the carrier of R by A83;
reconsider rkra = rk | ( the InternalRel of R -Seg a) as Element of PFuncs ( the carrier of R,(nextcard ac)) by PARTFUN1:45;
A88: rk . a = H . (a,rkra) by A78
.= sup (rng rkra) by A4 ;
A89: e in Y by ;
then reconsider rke = rk . e as Ordinal by ;
rke in rk .: Y by ;
then A90: inf (rk .: Y) c= rk . e by ORDINAL2:14;
rke in rng rkra by ;
hence contradiction by A85, A90, A88, ORDINAL1:5, ORDINAL2:19; :: thesis: verum