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 S_{1}[] 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_{1}( 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_{1}(x,p) in nextcard ac

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_{1}(x,p)
from FUNCT_7:sch 1(A1);

thus ( R is well_founded implies S_{1}[] )
:: 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 )_{1}[]
; :: 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 b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y ) )

assume that

A79: Y c= the carrier of R and

A80: Y <> {} ; :: thesis: ex b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y )

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: ( 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 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: verum

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 S

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

A1: for x being Element of the carrier of R

for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H

proof

consider H being Function of [: the carrier of R,(PFuncs ( the carrier of R,(nextcard ac))):],(nextcard ac) such that
let x be Element of the carrier of R; :: thesis: for p being Element of PFuncs ( the carrier of R,(nextcard ac)) holds H_{1}(x,p) in nextcard ac

let p be Element of PFuncs ( the carrier of R,(nextcard ac)); :: thesis: H_{1}(x,p) in nextcard ac

( 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_{1}(x,p) in nextcard ac
by A3, Th2; :: thesis: verum

end;let p be Element of PFuncs ( the carrier of R,(nextcard ac)); :: thesis: H

( 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

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

thus ( R is well_founded implies S

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
S
assume A5:
R is well_founded
; :: thesis: S_{1}[]

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 S_{2}[ 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_{2}[f] )
from WELLFND1:sch 1();

take ufs ; :: thesis: ufs is_recursively_expressed_by H

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 A24, A46; :: thesis: verum

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

$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

now :: thesis: for f, g being Function st f in fs & g in fs holds

f tolerates g

then reconsider ufs = union fs as Function by Th1;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: f tolerates g

reconsider ff = f, gg = g as PartFunc of the carrier of R,V by A7, A8, PARTFUN1:46;

defpred S_{3}[ 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: S_{3}[x]
by A9, A10, XBOOLE_0:def 4;

consider x0 being Element of R such that

A12: S_{3}[x0]
and

A13: for y being Element of R holds

( not x0 <> y or not S_{3}[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)

.= gg . x0 by A6, A8, A12 ;

hence contradiction by A12; :: thesis: verum

end;assume that

A7: f in fs and

A8: g in fs ; :: thesis: f tolerates g

reconsider ff = f, gg = g as PartFunc of the carrier of R,V by A7, A8, PARTFUN1:46;

defpred S

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: S

consider x0 being Element of R such that

A12: S

A13: for y being Element of R holds

( not x0 <> y or not S

ff | ( the InternalRel of R -Seg x0) = gg | ( the InternalRel of R -Seg x0)

proof

then ff . x0 =
H . [x0,(gg | ( the InternalRel of R -Seg x0))]
by A6, A7, A12
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 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: verum

end;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 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: verum

.= gg . x0 by A6, A8, A12 ;

hence contradiction by A12; :: thesis: verum

A24: now :: thesis: for x being set st x in dom ufs holds

ufs . x = H . [x,(ufs | ( the InternalRel of R -Seg x))]

A29:
dom ufs c= the carrier of R
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 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: verum

end;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 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: verum

proof

A34:
rng ufs c= V
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 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: verum

end;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 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: verum

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 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: verum

end;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 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: verum

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

A46:
dom ufs = the carrier of R
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 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: verum

end;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 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: verum

proof

then reconsider ufs = ufs as Function of the carrier of R,V by A34, FUNCT_2:def 1, RELSET_1:4;
defpred S_{3}[ 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 A29, A47;

A48: S_{3}[x]
by A47;

consider x0 being Element of R such that

A49: S_{3}[x0]
and

A50: for y being Element of R holds

( not x0 <> y or not S_{3}[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

dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= the carrier of R

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;

then [x0,(nf . x0)] in ufs by A61, TARSKI:def 4;

hence contradiction by A49, FUNCT_1:1; :: thesis: verum

end;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 A29, A47;

A48: S

consider x0 being Element of R such that

A49: S

A50: for y being Element of R holds

( not x0 <> y or not S

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

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;
ufs in PFuncs ( the carrier of R,V)
by A29, A34, PARTFUN1:def 3;

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 A34, FUNCT_4:17;

then A56: x in rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A54, XBOOLE_0:def 3;

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 A56, TARSKI:def 1;

hence contradiction by A55, A53, BINOP_1:17; :: thesis: verum

end;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 A34, FUNCT_4:17;

then A56: x in rng (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) by A54, XBOOLE_0:def 3;

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 A56, TARSKI:def 1;

hence contradiction by A55, A53, BINOP_1:17; :: thesis: verum

dom (ufs +* (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))) c= the carrier of R

proof

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;
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 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: verum

end;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 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: verum

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: for x being set st x in dom nf holds

nf . x = H . [x,(nf | ( the InternalRel of R -Seg x))]

dom nf is lower
nf . x = H . [x,(nf | ( the InternalRel of R -Seg x))]

let x be set ; :: thesis: ( x in dom nf implies nf . b_{1} = H . [b_{1},(nf | ( the InternalRel of R -Seg b_{1}))] )

assume A63: x in dom nf ; :: thesis: nf . b_{1} = H . [b_{1},(nf | ( the InternalRel of R -Seg b_{1}))]

end;assume A63: x in dom nf ; :: thesis: nf . b

per cases
( x in dom ufs or x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))])) )
by A57, A63, XBOOLE_0:def 3;

end;

suppose A64:
x in dom ufs
; :: thesis: nf . b_{1} = H . [b_{1},(nf | ( the InternalRel of R -Seg b_{1}))]

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

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: verum

end;proof

not x in dom (x0 .--> (H . [x0,(ufs | ( the InternalRel of R -Seg x0))]))
by A49, A64, TARSKI:def 1;
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 A66, TARSKI:def 1;

then [x0,x] in the InternalRel of R by A67, WELLORD1:1;

hence contradiction by A40, A49, A64; :: thesis: verum

end;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: verum

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: verum

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

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

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: verum

end;proof

A72:
x = x0
by A68, TARSKI:def 1;
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 A70, TARSKI:def 1;

hence contradiction by A71, WELLORD1:1; :: thesis: verum

end;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: verum

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: verum

proof

then
nf in fs
by A6, A62;
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 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: verum

end;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 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: verum

then [x0,(nf . x0)] in ufs by A61, TARSKI:def 4;

hence contradiction by A49, FUNCT_1:1; :: thesis: verum

take ufs ; :: thesis: ufs is_recursively_expressed_by H

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 A24, A46; :: thesis: verum

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 b

( b

assume that

A79: Y c= the carrier of R and

A80: Y <> {} ; :: thesis: ex b

( b

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: ( 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 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: verum