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 = --> a0;
set F2 = ( the carrier of R --> a1) +* ( --> a0);
defpred S1[ 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: 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 S1[x,y,u]
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 S1[u,b3,b4]
let y be Element of PFuncs ( the carrier of R,V); :: thesis: ex u being Element of {a0,a1} st S1[u,b2,b3]
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 ) )
;
suppose A6: ex x being set st
( x in dom y & y . x = a1 ) ; :: thesis: ex u being Element of {a0,a1} st S1[u,b2,b3]
take u = u; :: thesis: S1[x,y,u]
thus S1[x,y,u] by A6; :: thesis: verum
end;
suppose A7: for x being set holds
( not x in dom y or not y . x = a1 ) ; :: thesis: ex v being Element of {a0,a1} st S1[v,b2,b3]
take v = v; :: thesis: S1[x,y,v]
thus S1[x,y,v] by A3, A7; :: thesis: verum
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 S1[x,y,H . (x,y)] from A9: {a0,a1} c= V by ;
then A10: rng H c= V ;
(rng ( the carrier of R --> a1)) \/ (rng ( --> a0)) c= {a0} \/ {a1} by XBOOLE_1:13;
then A11: (rng ( the carrier of R --> a1)) \/ (rng ( --> a0)) c= {a0,a1} by ENUMSET1:1;
rng (( the carrier of R --> a1) +* ( --> a0)) c= (rng ( the carrier of R --> a1)) \/ (rng ( --> a0)) by FUNCT_4:17;
then rng (( the carrier of R --> a1) +* ( --> a0)) c= {a0,a1} by A11;
then A12: rng (( the carrier of R --> a1) +* ( --> 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 ;
A15: dom ( --> a0) = well_founded-Part R ;
A16: dom (( the carrier of R --> a1) +* ( --> a0)) = (dom ( the carrier of R --> a1)) \/ (dom ( --> a0)) by FUNCT_4:def 1
.= the carrier of R by XBOOLE_1:12 ;
then reconsider F2 = ( the carrier of R --> a1) +* ( --> a0) as Function of the carrier of R,V by ;
A17: F2 is_recursively_expressed_by H
proof
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;
per cases ( x in well_founded-Part R or not x in well_founded-Part R ) ;
suppose A18: x in well_founded-Part R ; :: thesis: F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x)))
now :: thesis: for z being set st z in dom F2r holds
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 ;
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
.= ( --> a0) . z by
.= a0 by ;
hence F2r . z <> a1 by A3; :: thesis: verum
end;
then A21: H . (x,F2r) <> a1 by A8;
A22: H . [x,F2r] in rng H by ;
((well_founded-Part R) --> a0) . x = a0 by ;
hence F2 . x = a0 by
.= H . (x,(F2 | ( the InternalRel of R -Seg x))) by ;
:: thesis: verum
end;
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 ;
A28: F2r . z = F2 . z by
.= ( the carrier of R --> a1) . z by
.= a1 by ;
thus F2 . x = ( the carrier of R --> a1) . x by
.= a1
.= H . (x,(F2 | ( the InternalRel of R -Seg x))) by A8, A27, A28 ; :: thesis: verum
end;
end;
end;
reconsider F1 = the carrier of R --> a0 as Function of the carrier of R,V by ;
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
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 ;
now :: thesis: for z being set st z in dom F1r holds
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 ;
hence F1r . z <> a1 by A3; :: thesis: verum
end;
then A34: H . (x,F1r) <> a1 by A8;
thus F1 . x = a0
.= H . (x,(F1 | ( the InternalRel of R -Seg x))) by ; :: thesis: verum
end;
A35: F1 . x = a0 by ;
F2 . x = ( the carrier of R --> a1) . x by
.= a1 by ;
hence contradiction by A3, A31, A17, A29, A35; :: thesis: verum