let R be non empty well_founded RelStr ; for V being non empty 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
let V be non empty 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
set c = the carrier of R;
set r = the InternalRel of R;
let H be 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
let F1, F2 be Function of the carrier of R,V; ( F1 is_recursively_expressed_by H & F2 is_recursively_expressed_by H implies F1 = F2 )
assume that
A1:
F1 is_recursively_expressed_by H
and
A2:
F2 is_recursively_expressed_by H
; F1 = F2
defpred S1[ set ] means F1 . $1 <> F2 . $1;
A3:
dom F2 = the carrier of R
by FUNCT_2:def 1;
assume
F1 <> F2
; contradiction
then consider x being Element of the carrier of R such that
A4:
F1 . x <> F2 . x
by FUNCT_2:63;
reconsider x = x as Element of R ;
A5:
R is well_founded
;
A6:
S1[x]
by A4;
consider x0 being Element of R such that
A7:
S1[x0]
and
A8:
for y being Element of R holds
( not x0 <> y or not S1[y] or not [y,x0] in the InternalRel of R )
from WELLFND1:sch 2(A6, A5);
A9:
dom F1 = the carrier of R
by FUNCT_2:def 1;
F1 | ( the InternalRel of R -Seg x0) = F2 | ( the InternalRel of R -Seg x0)
proof
set fr =
F1 | ( the InternalRel of R -Seg x0);
set gr =
F2 | ( the InternalRel of R -Seg x0);
assume A10:
not
F1 | ( the InternalRel of R -Seg x0) = F2 | ( the InternalRel of R -Seg x0)
;
contradiction
A11:
dom (F1 | ( the InternalRel of R -Seg x0)) = the
InternalRel of
R -Seg x0
by A9, Th3, RELAT_1:62;
dom (F2 | ( the InternalRel of R -Seg x0)) = the
InternalRel of
R -Seg x0
by A3, Th3, RELAT_1:62;
then consider x1 being
object such that A12:
x1 in dom (F1 | ( the InternalRel of R -Seg x0))
and A13:
(F1 | ( the InternalRel of R -Seg x0)) . x1 <> (F2 | ( the InternalRel of R -Seg x0)) . x1
by A11, A10;
A14:
[x1,x0] in the
InternalRel of
R
by A11, A12, WELLORD1:1;
reconsider x1 =
x1 as
Element of
R by A12;
A15:
x1 <> x0
by A11, A12, WELLORD1:1;
(
(F1 | ( the InternalRel of R -Seg x0)) . x1 = F1 . x1 &
(F2 | ( the InternalRel of R -Seg x0)) . x1 = F2 . x1 )
by A11, A12, FUNCT_1:49;
hence
contradiction
by A8, A13, A14, A15;
verum
end;
then F1 . x0 =
H . (x0,(F2 | ( the InternalRel of R -Seg x0)))
by A1
.=
F2 . x0
by A2
;
hence
contradiction
by A7; verum