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 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₁[ 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};

A5: now :: thesis:

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

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

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

end;

suppose A7: 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 A3, A7; :: thesis:

end;

end;

end;

consider H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],{a0,a1} such that
A8: 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(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

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

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

let z be set ; :: thesis:
A19: the InternalRel of R -Seg x c= well_founded-Part R by A18, Th4;
assume z in dom F2r ; :: thesis:
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:

end;

then A21: H . (x,F2r) <> a1 by A8;
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:

end;

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

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:

end;

end;

end;

reconsider F1 = the carrier of R --> a0 as Function of the carrier of R,V by A1, FUNCOP_1:45;
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:
assume not R is well_founded ; :: thesis:
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

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:45;
A32: H . [x,F1r] in rng H by A14, FUNCT_1:def 3;

let z be set ; :: thesis:
assume A33: z in dom F1r ; :: thesis:
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:

end;

then A34: H . (x,F1r) <> a1 by A8;
thus F1 . x = a0
.= H . (x,(F1 | ( the InternalRel of R -Seg x))) by A13, A34, A32, TARSKI:def 2 ; :: thesis:

end;

A35: F1 . x = a0 by A30, FUNCOP_1:7;
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: