let R be non empty RelStr ; :: thesis:
let V be non trivial set ; :: thesis:
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 set such that
A1: ( a0 in V & a1 in V & a0 <> a1 ) by REALSET1:14;
set a01 = {a0,a1};
A2: {a0,a1} c= V by A1, ZFMISC_1:38;
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);
A3: dom (the carrier of R --> a1) = the carrier of R by FUNCOP_1:19;
A4: dom ((well_founded-Part R) --> a0) = well_founded-Part R by FUNCOP_1:19;
A5: 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 A3, A4, XBOOLE_1:12 ;
reconsider F1 = the carrier of R --> a0 as Function of the carrier of R,V by A1, FUNCOP_1:57;
(rng (the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0} \/ {a1} by XBOOLE_1:13;
then ( (rng (the carrier of R --> a1)) \/ (rng ((well_founded-Part R) --> a0)) c= {a0,a1} & 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 ENUMSET1:41, FUNCT_4:18;
then rng ((the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= {a0,a1} by XBOOLE_1:1;
then rng ((the carrier of R --> a1) +* ((well_founded-Part R) --> a0)) c= V by A2, XBOOLE_1:1;
then reconsider F2 = (the carrier of R --> a1) +* ((well_founded-Part R) --> a0) as Function of the carrier of R,V by A5, FUNCT_2:def 1, RELSET_1:11;
defpred S₁[ set , Function, set ] means ( ex x being set st
( x in dom $2 & $2 . x = a1 ) iff $3 = a1 );

A6: now

let x be Element of the carrier of R; :: thesis:
let y be Element of PFuncs the carrier of R,V; :: thesis:
reconsider u = a1, v = a0 as Element of {a0,a1} by TARSKI:def 2;

per cases ;

suppose A7: ex x being set st
( x in dom y & y . x = a1 ) ; :: thesis:

take u = u; :: thesis:
thus S₁[x,y,u] by A7; :: thesis:

end;

suppose A8: for x being set holds
( not x in dom y or not y . x = a1 ) ; :: thesis:

take v = v; :: thesis:
thus S₁[x,y,v] by A1, A8; :: thesis:

end;

consider H being Function of [:the carrier of R,(PFuncs the carrier of R,V):],{a0,a1} such that
A9: for x being Element of the carrier of R
for y being Element of PFuncs the carrier of R,V holds S₁[x,y,H . x,y] from BINOP_1:sch 3(A6);
A10: rng H c= {a0,a1} ;
A11: ( dom H = [:the carrier of R,(PFuncs the carrier of R,V):] & rng H c= V ) by A2, FUNCT_2:def 1, XBOOLE_1:1;
then reconsider H = H as Function of [:the carrier of R,(PFuncs the carrier of R,V):],V by FUNCT_2:def 1, RELSET_1:11;
A12: F1 is_recursively_expressed_by H

proof

let x be Element of the carrier of R; :: according to WELLFND1:def 5 :: thesis:
reconsider F1r = F1 | (the InternalRel of R -Seg x) as Element of PFuncs the carrier of R,V by PARTFUN1:119;

now

let z be set ; :: thesis:
assume A13: z in dom F1r ; :: thesis:
then ( z in the InternalRel of R -Seg x & z in dom F1 ) by RELAT_1:86;
then F1r . z = F1 . z by FUNCT_1:72
.= a0 by A13, FUNCOP_1:13 ;
hence F1r . z <> a1 by A1; :: thesis:

end;

then A14: H . x,F1r <> a1 by A9;
A15: H . [x,F1r] in rng H by A11, FUNCT_1:def 5;
thus F1 . x = a0 by FUNCOP_1:13
.= H . x,(F1 | (the InternalRel of R -Seg x)) by A10, A14, A15, TARSKI:def 2 ; :: thesis:

end;

A16: F2 is_recursively_expressed_by H

proof

let x be Element of the carrier of R; :: according to WELLFND1:def 5 :: thesis:
reconsider F2r = F2 | (the InternalRel of R -Seg x) as Element of PFuncs the carrier of R,V by PARTFUN1:119;

per cases ;

suppose A17: x in well_founded-Part R ; :: thesis:

now

let z be set ; :: thesis:
assume z in dom F2r ; :: thesis:
then A18: ( z in the InternalRel of R -Seg x & z in dom F2 ) by RELAT_1:86;
A19: the InternalRel of R -Seg x c= well_founded-Part R by A17, Th5;
F2r . z = F2 . z by A18, FUNCT_1:72
.= ((well_founded-Part R) --> a0) . z by A4, A18, A19, FUNCT_4:14
.= a0 by A18, A19, FUNCOP_1:13 ;
hence F2r . z <> a1 by A1; :: thesis:

end;

then A20: H . x,F2r <> a1 by A9;
A21: H . [x,F2r] in rng H by A11, FUNCT_1:def 5;
((well_founded-Part R) --> a0) . x = a0 by A17, FUNCOP_1:13;
hence F2 . x = a0 by A4, A17, FUNCT_4:14
.= H . x,(F2 | (the InternalRel of R -Seg x)) by A10, A20, A21, TARSKI:def 2 ;
:: thesis:

end;

suppose A22: not x in well_founded-Part R ; :: thesis:

then not the InternalRel of R -Seg x c= well_founded-Part R by Th10;
then consider z being set such that
A23: ( z in the InternalRel of R -Seg x & not z in well_founded-Part R ) by TARSKI:def 3;
A24: the InternalRel of R -Seg x c= the carrier of R by Th4;
then A25: z in dom F2r by A5, A23, RELAT_1:86;
A26: F2r . z = F2 . z by A23, FUNCT_1:72
.= (the carrier of R --> a1) . z by A4, A23, FUNCT_4:12
.= a1 by A23, A24, FUNCOP_1:13 ;
thus F2 . x = (the carrier of R --> a1) . x by A4, A22, FUNCT_4:12
.= a1 by FUNCOP_1:13
.= H . x,(F2 | (the InternalRel of R -Seg x)) by A9, A25, A26 ; :: thesis:

end;

assume A27: 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:
assume not R is well_founded ; :: thesis:
then well_founded-Part R <> the carrier of R by Th9;
then consider x being set such that
A28: ( ( 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;
A29: F1 . x = a0 by A28, FUNCOP_1:13;
F2 . x = (the carrier of R --> a1) . x by A4, A28, FUNCT_4:12
.= a1 by A28, FUNCOP_1:13 ;
hence contradiction by A1, A12, A16, A27, A29; :: thesis: