let R be non empty RelStr ; :: thesis: for V being non trivial set st ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V

for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds

F1 = F2 ) holds

R is well_founded

let V be non trivial set ; :: thesis: ( ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V

for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds

F1 = F2 ) implies R is well_founded )

set c = the carrier of R;

set r = the InternalRel of R;

set PF = PFuncs ( the carrier of R,V);

set wfp = well_founded-Part R;

consider a0, a1 being object such that

A1: a0 in V and

A2: a1 in V and

A3: a0 <> a1 by ZFMISC_1:def 10;

set F3 = the carrier of R --> a1;

set F4 = (well_founded-Part R) --> a0;

set F2 = ( the carrier of R --> a1) +* ((well_founded-Part R) --> a0);

defpred S_{1}[ set , Function, set ] means ( ex x being set st

( x in dom $2 & $2 . x = a1 ) iff $3 = a1 );

reconsider a0 = a0, a1 = a1 as set by TARSKI:1;

set a01 = {a0,a1};

A8: for x being Element of the carrier of R

for y being Element of PFuncs ( the carrier of R,V) holds S_{1}[x,y,H . (x,y)]
from BINOP_1:sch 3(A5);

A9: {a0,a1} c= V by A1, A2, ZFMISC_1:32;

then A10: rng H c= V ;

(rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0} \/ {a1} by XBOOLE_1:13;

then A11: (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0,a1} by ENUMSET1:1;

rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) by FUNCT_4:17;

then rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= {a0,a1} by A11;

then A12: rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= V by A9;

A13: rng H c= {a0,a1} ;

A14: dom H = [: the carrier of R,(PFuncs ( the carrier of R,V)):] by FUNCT_2:def 1;

then reconsider H = H as Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V by A10, FUNCT_2:def 1, RELSET_1:4;

A15: dom ((well_founded-Part R) --> a0) = well_founded-Part R ;

A16: dom (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) = (dom ( the carrier of R --> a1)) \/ (dom ((well_founded-Part R) --> a0)) by FUNCT_4:def 1

.= the carrier of R by XBOOLE_1:12 ;

then reconsider F2 = ( the carrier of R --> a1) +* ((well_founded-Part R) --> a0) as Function of the carrier of R,V by A12, FUNCT_2:def 1, RELSET_1:4;

A17: F2 is_recursively_expressed_by H

assume A29: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V

for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds

F1 = F2 ; :: thesis: R is well_founded

assume not R is well_founded ; :: thesis: contradiction

then well_founded-Part R <> the carrier of R by Th8;

then consider x being object such that

A30: ( ( x in well_founded-Part R & not x in the carrier of R ) or ( x in the carrier of R & not x in well_founded-Part R ) ) by TARSKI:2;

A31: F1 is_recursively_expressed_by H

F2 . x = ( the carrier of R --> a1) . x by A15, A30, FUNCT_4:11

.= a1 by A30, FUNCOP_1:7 ;

hence contradiction by A3, A31, A17, A29, A35; :: thesis: verum

for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds

F1 = F2 ) holds

R is well_founded

let V be non trivial set ; :: thesis: ( ( for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V

for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds

F1 = F2 ) implies R is well_founded )

set c = the carrier of R;

set r = the InternalRel of R;

set PF = PFuncs ( the carrier of R,V);

set wfp = well_founded-Part R;

consider a0, a1 being object such that

A1: a0 in V and

A2: a1 in V and

A3: a0 <> a1 by ZFMISC_1:def 10;

set F3 = the carrier of R --> a1;

set F4 = (well_founded-Part R) --> a0;

set F2 = ( the carrier of R --> a1) +* ((well_founded-Part R) --> a0);

defpred S

( x in dom $2 & $2 . x = a1 ) iff $3 = a1 );

reconsider a0 = a0, a1 = a1 as set by TARSKI:1;

set a01 = {a0,a1};

A5: now :: thesis: for x being Element of the carrier of R

for y being Element of PFuncs ( the carrier of R,V) ex u being Element of {a0,a1} st S_{1}[x,y,u]

consider H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],{a0,a1} such that for y being Element of PFuncs ( the carrier of R,V) ex u being Element of {a0,a1} st S

reconsider u = a1, v = a0 as Element of {a0,a1} by TARSKI:def 2;

let x be Element of the carrier of R; :: thesis: for y being Element of PFuncs ( the carrier of R,V) ex u being Element of {a0,a1} st S_{1}[u,b_{3},b_{4}]

let y be Element of PFuncs ( the carrier of R,V); :: thesis: ex u being Element of {a0,a1} st S_{1}[u,b_{2},b_{3}]

end;let x be Element of the carrier of R; :: thesis: for y being Element of PFuncs ( the carrier of R,V) ex u being Element of {a0,a1} st S

let y be Element of PFuncs ( the carrier of R,V); :: thesis: ex u being Element of {a0,a1} st S

per cases
( ex x being set st

( x in dom y & y . x = a1 ) or for x being set holds

( not x in dom y or not y . x = a1 ) ) ;

end;

( x in dom y & y . x = a1 ) or for x being set holds

( not x in dom y or not y . x = a1 ) ) ;

suppose A6:
ex x being set st

( x in dom y & y . x = a1 ) ; :: thesis: ex u being Element of {a0,a1} st S_{1}[u,b_{2},b_{3}]

end;

( x in dom y & y . x = a1 ) ; :: thesis: ex u being Element of {a0,a1} st S

end;

A8: for x being Element of the carrier of R

for y being Element of PFuncs ( the carrier of R,V) holds S

A9: {a0,a1} c= V by A1, A2, ZFMISC_1:32;

then A10: rng H c= V ;

(rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0} \/ {a1} by XBOOLE_1:13;

then A11: (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0,a1} by ENUMSET1:1;

rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= (rng ( the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) by FUNCT_4:17;

then rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= {a0,a1} by A11;

then A12: rng (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= V by A9;

A13: rng H c= {a0,a1} ;

A14: dom H = [: the carrier of R,(PFuncs ( the carrier of R,V)):] by FUNCT_2:def 1;

then reconsider H = H as Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V by A10, FUNCT_2:def 1, RELSET_1:4;

A15: dom ((well_founded-Part R) --> a0) = well_founded-Part R ;

A16: dom (( the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) = (dom ( the carrier of R --> a1)) \/ (dom ((well_founded-Part R) --> a0)) by FUNCT_4:def 1

.= the carrier of R by XBOOLE_1:12 ;

then reconsider F2 = ( the carrier of R --> a1) +* ((well_founded-Part R) --> a0) as Function of the carrier of R,V by A12, FUNCT_2:def 1, RELSET_1:4;

A17: F2 is_recursively_expressed_by H

proof

reconsider F1 = the carrier of R --> a0 as Function of the carrier of R,V by A1, FUNCOP_1:45;
let x be Element of the carrier of R; :: according to WELLFND1:def 5 :: thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x)))

reconsider F2r = F2 | ( the InternalRel of R -Seg x) as Element of PFuncs ( the carrier of R,V) by PARTFUN1:45;

end;reconsider F2r = F2 | ( the InternalRel of R -Seg x) as Element of PFuncs ( the carrier of R,V) by PARTFUN1:45;

per cases
( x in well_founded-Part R or not x in well_founded-Part R )
;

end;

suppose A18:
x in well_founded-Part R
; :: thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x)))

A22: H . [x,F2r] in rng H by A14, FUNCT_1:def 3;

((well_founded-Part R) --> a0) . x = a0 by A18, FUNCOP_1:7;

hence F2 . x = a0 by A15, A18, FUNCT_4:13

.= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A13, A21, A22, TARSKI:def 2 ;

:: thesis: verum

end;

now :: thesis: for z being set st z in dom F2r holds

F2r . z <> a1

then A21:
H . (x,F2r) <> a1
by A8;F2r . z <> a1

let z be set ; :: thesis: ( z in dom F2r implies F2r . z <> a1 )

A19: the InternalRel of R -Seg x c= well_founded-Part R by A18, Th4;

assume z in dom F2r ; :: thesis: F2r . z <> a1

then A20: z in the InternalRel of R -Seg x by RELAT_1:57;

then F2r . z = F2 . z by FUNCT_1:49

.= ((well_founded-Part R) --> a0) . z by A15, A20, A19, FUNCT_4:13

.= a0 by A20, A19, FUNCOP_1:7 ;

hence F2r . z <> a1 by A3; :: thesis: verum

end;A19: the InternalRel of R -Seg x c= well_founded-Part R by A18, Th4;

assume z in dom F2r ; :: thesis: F2r . z <> a1

then A20: z in the InternalRel of R -Seg x by RELAT_1:57;

then F2r . z = F2 . z by FUNCT_1:49

.= ((well_founded-Part R) --> a0) . z by A15, A20, A19, FUNCT_4:13

.= a0 by A20, A19, FUNCOP_1:7 ;

hence F2r . z <> a1 by A3; :: thesis: verum

A22: H . [x,F2r] in rng H by A14, FUNCT_1:def 3;

((well_founded-Part R) --> a0) . x = a0 by A18, FUNCOP_1:7;

hence F2 . x = a0 by A15, A18, FUNCT_4:13

.= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A13, A21, A22, TARSKI:def 2 ;

:: thesis: verum

suppose A23:
not x in well_founded-Part R
; :: thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x)))

then
not the InternalRel of R -Seg x c= well_founded-Part R
by Th9;

then consider z being object such that

A24: z in the InternalRel of R -Seg x and

A25: not z in well_founded-Part R ;

A26: the InternalRel of R -Seg x c= the carrier of R by Th3;

then A27: z in dom F2r by A16, A24, RELAT_1:57;

A28: F2r . z = F2 . z by A24, FUNCT_1:49

.= ( the carrier of R --> a1) . z by A15, A25, FUNCT_4:11

.= a1 by A24, A26, FUNCOP_1:7 ;

thus F2 . x = ( the carrier of R --> a1) . x by A15, A23, FUNCT_4:11

.= a1

.= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A8, A27, A28 ; :: thesis: verum

end;then consider z being object such that

A24: z in the InternalRel of R -Seg x and

A25: not z in well_founded-Part R ;

A26: the InternalRel of R -Seg x c= the carrier of R by Th3;

then A27: z in dom F2r by A16, A24, RELAT_1:57;

A28: F2r . z = F2 . z by A24, FUNCT_1:49

.= ( the carrier of R --> a1) . z by A15, A25, FUNCT_4:11

.= a1 by A24, A26, FUNCOP_1:7 ;

thus F2 . x = ( the carrier of R --> a1) . x by A15, A23, FUNCT_4:11

.= a1

.= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A8, A27, A28 ; :: thesis: verum

assume A29: for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V

for F1, F2 being Function of the carrier of R,V st F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H holds

F1 = F2 ; :: thesis: R is well_founded

assume not R is well_founded ; :: thesis: contradiction

then well_founded-Part R <> the carrier of R by Th8;

then consider x being object such that

A30: ( ( x in well_founded-Part R & not x in the carrier of R ) or ( x in the carrier of R & not x in well_founded-Part R ) ) by TARSKI:2;

A31: F1 is_recursively_expressed_by H

proof

A35:
F1 . x = a0
by A30, FUNCOP_1:7;
let x be Element of the carrier of R; :: according to WELLFND1:def 5 :: thesis: F1 . x = H . (x,(F1 | ( the InternalRel of R -Seg x)))

reconsider F1r = F1 | ( the InternalRel of R -Seg x) as Element of PFuncs ( the carrier of R,V) by PARTFUN1:45;

A32: H . [x,F1r] in rng H by A14, FUNCT_1:def 3;

thus F1 . x = a0

.= H . (x,(F1 | ( the InternalRel of R -Seg x))) by A13, A34, A32, TARSKI:def 2 ; :: thesis: verum

end;reconsider F1r = F1 | ( the InternalRel of R -Seg x) as Element of PFuncs ( the carrier of R,V) by PARTFUN1:45;

A32: H . [x,F1r] in rng H by A14, FUNCT_1:def 3;

now :: thesis: for z being set st z in dom F1r holds

F1r . z <> a1

then A34:
H . (x,F1r) <> a1
by A8;F1r . z <> a1

let z be set ; :: thesis: ( z in dom F1r implies F1r . z <> a1 )

assume A33: z in dom F1r ; :: thesis: F1r . z <> a1

then z in the InternalRel of R -Seg x by RELAT_1:57;

then F1r . z = F1 . z by FUNCT_1:49

.= a0 by A33, FUNCOP_1:7 ;

hence F1r . z <> a1 by A3; :: thesis: verum

end;assume A33: z in dom F1r ; :: thesis: F1r . z <> a1

then z in the InternalRel of R -Seg x by RELAT_1:57;

then F1r . z = F1 . z by FUNCT_1:49

.= a0 by A33, FUNCOP_1:7 ;

hence F1r . z <> a1 by A3; :: thesis: verum

thus F1 . x = a0

.= H . (x,(F1 | ( the InternalRel of R -Seg x))) by A13, A34, A32, TARSKI:def 2 ; :: thesis: verum

F2 . x = ( the carrier of R --> a1) . x by A15, A30, FUNCT_4:11

.= a1 by A30, FUNCOP_1:7 ;

hence contradiction by A3, A31, A17, A29, A35; :: thesis: verum