let R be non empty RelStr ; 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 ; ( ( 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 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 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;
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);
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 )
;
ex u being Element of {a0,a1} st S1[u,b2,b3]take u =
u;
S1[x,y,u]thus
S1[
x,
y,
u]
by A6;
verum end; suppose A7:
for
x being
set holds
( not
x in dom y or not
y . x = a1 )
;
ex v being Element of {a0,a1} st S1[v,b2,b3]take v =
v;
S1[x,y,v]thus
S1[
x,
y,
v]
by A3, A7;
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 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
proof
let x be
Element of the
carrier of
R;
WELLFND1:def 5 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
;
F2 . x = H . (x,(F2 | ( the InternalRel of R -Seg x)))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
;
verum end; suppose A23:
not
x in well_founded-Part R
;
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
;
verum 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
; R is well_founded
assume
not R is well_founded
; 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
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; verum