let R be non empty RelStr ; :: thesis:
set c = the carrier of R;
set r = the InternalRel of R;
defpred S₁[] 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 H₁( 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 H₁(x,p) in nextcard ac

proof

let x be Element of the carrier of R; :: thesis:
let p be Element of PFuncs ( the carrier of R,(nextcard ac)); :: thesis:
( card (dom p) c= card the carrier of R & card (rng p) c= card (dom p) ) by CARD_1:11, CARD_1:12;
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 CARD_1:18, ORDINAL1:12;
nextcard ac is regular by CARD_5:30;
hence H₁(x,p) in nextcard ac by A3, Th2; :: thesis:

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) = H₁(x,p) from FUNCT_7:sch 1(A1);
thus ( R is well_founded implies S₁[] ) :: thesis:

proof

assume A5: R is well_founded ; :: thesis:
let V be non empty set ; :: thesis:
let H be Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V; :: thesis:
defpred S₂[ 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 S₂[f] ) from WELLFND1:sch 1();

now :: thesis:

let f, g be Function; :: thesis:
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 A7, A8, PARTFUN1:46;
defpred S₃[ set ] means ( $1 in dom ff & $1 in dom gg & ff . $1 <> gg . $1 );
assume not f tolerates g ; :: thesis:
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: S₃[x] by A9, A10, XBOOLE_0:def 4;
consider x0 being Element of R such that
A12: S₃[x0] and
A13: for y being Element of R holds
( not x0 <> y or not S₃[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch 2(A11, A5);
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:
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 A12, Th4, RELAT_1:62;
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 A12, A16, Th4, RELAT_1:62;
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 A16, A18, WELLORD1:1;
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 A16, A18, FUNCT_1:49;
A22: x1 <> x0 by A16, A18, WELLORD1:1;
A23: x1 in dom gg by A12, A17, A20;
x1 in dom ff by A12, A15, A20;
hence contradiction by A13, A19, A20, A21, A22, A23; :: thesis:

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:

end;

then reconsider ufs = union fs as Function by Th1;

A24: now :: thesis:

let x be set ; :: thesis:
assume x in dom ufs ; :: thesis:
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 A26, PARTFUN1:46;
A27: x in dom ff by A25, FUNCT_1:1;
A28: ( dom ff is lower & ff c= ufs ) by A6, A26, ZFMISC_1:74;
thus ufs . x = ff . x by A25, FUNCT_1:1
.= H . [x,(ff | ( the InternalRel of R -Seg x))] by A6, A26, A27
.= H . [x,(ufs | ( the InternalRel of R -Seg x))] by A27, A28, Th4, GRFUNC_1:27 ; :: thesis:

end;

A29: dom ufs c= the carrier of R

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in dom ufs ; :: thesis:
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 A31, PARTFUN1:def 3;
y in dom ff by A30, A32, XTUPLE_0:def 12;
hence y in the carrier of R by A33; :: thesis:

end;

A34: rng ufs c= V

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng ufs ; :: thesis:
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 A35, FUNCT_1:1;
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 A37, PARTFUN1:def 3;
y in rng ff by A36, A38, XTUPLE_0:def 13;
hence y in V by A39; :: thesis:

end;

A40: now :: thesis:

let x, y be object ; :: thesis:
assume that
A41: x in dom ufs and
A42: [y,x] in the InternalRel of R ; :: thesis:
[x,(ufs . x)] in ufs by A41, FUNCT_1:1;
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 A44, PARTFUN1:46;
ff c= ufs by A44, ZFMISC_1:74;
then A45: dom ff c= dom ufs by GRFUNC_1:2;
( dom ff is lower & x in dom ff ) by A6, A43, A44, FUNCT_1:1;
then y in dom ff by A42;
hence y in dom ufs by A45; :: thesis:

end;

A46: dom ufs = the carrier of R

proof

defpred S₃[ set ] means ( $1 in the carrier of R & not $1 in dom ufs );
assume dom ufs <> the carrier of R ; :: thesis:
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 A29, A47;
A48: S₃[x] by A47;
consider x0 being Element of R such that
A49: S₃[x0] and
A50: for y being Element of R holds
( not x0 <> y or not S₃[y] or not [y,x0] in the InternalRel of R ) from WELLFND1:sch 2(A48, A5);
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

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:
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:
not x in dom ufs by A29, A59;
then x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A58, XBOOLE_0:def 3;
hence contradiction by A51, A59; :: thesis:

end;

then A60: ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) in PFuncs ( the carrier of R,V) by A52, PARTFUN1:def 3;
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 A57, XBOOLE_0:def 3;
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 A60, PARTFUN1:46;

A62: now :: thesis:

let x be set ; :: thesis:
assume A63: x in dom nf ; :: thesis:

per cases by A57, A63, XBOOLE_0:def 3;

suppose A64: x in dom ufs ; :: thesis:

A65: {x0} misses the InternalRel of R -Seg x

proof

assume {x0} meets the InternalRel of R -Seg x ; :: thesis:
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 A66, TARSKI:def 1;
then [x0,x] in the InternalRel of R by A67, WELLORD1:1;
hence contradiction by A40, A49, A64; :: thesis:

end;

not x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A49, A64, TARSKI:def 1;
hence nf . x = ufs . x by FUNCT_4:11
.= H . [x,(ufs | ( the InternalRel of R -Seg x))] by A24, A64
.= H . [x,(nf | ( the InternalRel of R -Seg x))] by A51, A65, FUNCT_4:72 ;
:: thesis:

end;

suppose A68: x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) ; :: thesis:

A69: {x0} misses the InternalRel of R -Seg x0

proof

assume {x0} meets the InternalRel of R -Seg x0 ; :: thesis:
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 A70, TARSKI:def 1;
hence contradiction by A71, WELLORD1:1; :: thesis:

end;

A72: x = x0 by A68, TARSKI:def 1;
hence nf . x = (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) . x0 by A68, FUNCT_4:13
.= H . [x0,(ufs | ( the InternalRel of R -Seg x0))] by FUNCOP_1:72
.= H . [x,(nf | ( the InternalRel of R -Seg x))] by A51, A72, A69, FUNCT_4:72 ;
:: thesis:

end;

dom nf is lower

proof

let x, y be object ; :: according to WELLFND1:def 1 :: thesis:
assume that
A73: x in dom nf and
A74: [y,x] in the InternalRel of R ; :: thesis:
assume A75: not y in dom nf ; :: thesis:
then A76: not y in dom ufs by A57, XBOOLE_0:def 3;
then not x in dom ufs by A40, A74;
then x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A73, XBOOLE_0:def 3;
then A77: x = x0 by TARSKI:def 1;
reconsider y = y as Element of R by A74, ZFMISC_1:87;
not y in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A57, A75, XBOOLE_0:def 3;
then y <> x0 by TARSKI:def 1;
hence contradiction by A50, A74, A76, A77; :: thesis:

end;

then nf in fs by A6, A62;
then [x0,(nf . x0)] in ufs by A61, TARSKI:def 4;
hence contradiction by A49, FUNCT_1:1; :: thesis:

end;

then reconsider ufs = ufs as Function of the carrier of R,V by A34, FUNCT_2:def 1, RELSET_1:4;
take ufs ; :: thesis:
let x be Element of the carrier of R; :: according to WELLFND1:def 5 :: thesis:
thus ufs . x = H . (x,(ufs | ( the InternalRel of R -Seg x))) by A24, A46; :: thesis:

end;

assume S₁[] ; :: thesis:
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:
assume that
A79: Y c= the carrier of R and
A80: Y <> {} ; :: thesis:
set m = inf (rk .: Y);
consider b being object such that
A81: b in Y by A80, XBOOLE_0:def 1;
A82: dom rk = the carrier of R by FUNCT_2:def 1;
then rk . b in rk .: Y by A79, A81, FUNCT_1:def 6;
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:
thus a in Y by A84; :: thesis:
assume ( the InternalRel of R -Seg a) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis:
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 A86, XBOOLE_0:def 4;
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 A86, XBOOLE_0:def 4;
then reconsider rke = rk . e as Ordinal by A79, FUNCT_2:5, ORDINAL1:13;
rke in rk .: Y by A82, A79, A89, FUNCT_1:def 6;
then A90: inf (rk .: Y) c= rk . e by ORDINAL2:14;
rke in rng rkra by A82, A79, A87, A89, FUNCT_1:50;
hence contradiction by A85, A90, A88, ORDINAL1:5, ORDINAL2:19; :: thesis: