let R be non empty well_founded RelStr ; :: thesis: 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 ; :: 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
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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: F1 = F2
defpred S₁[ set ] means F1 . $1 <> F2 . $1;
A3: dom F2 = the carrier of R by FUNCT_2:def 1;
assume F1 <> F2 ; :: thesis: 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: S₁[x] by A4;
consider x0 being Element of R such that
A7: S₁[x0] and
A8: for y being Element of R holds
( not x0 <> y or not S₁[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) ; :: thesis: 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; :: thesis: verum

end;

then F1 . x0 = H . (x0,(F2 | ( the InternalRel of R -Seg x0))) by A1
.= F2 . x0 by A2 ;
hence contradiction by A7; :: thesis: verum