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
A3: ( dom F1 = the carrier of R & 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:113;
reconsider x = x as Element of R ;
defpred S₁[ set ] means F1 . $1 <> F2 . $1;
A5: S₁[x] by A4;
A6: R is well_founded ;
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(A5, A6);
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);
A9: ( dom (F1 | (the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 & dom (F2 | (the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 ) by A3, Th4, RELAT_1:91;
assume not F1 | (the InternalRel of R -Seg x0) = F2 | (the InternalRel of R -Seg x0) ; :: thesis: contradiction
then consider x1 being set such that
A10: ( x1 in dom (F1 | (the InternalRel of R -Seg x0)) & (F1 | (the InternalRel of R -Seg x0)) . x1 <> (F2 | (the InternalRel of R -Seg x0)) . x1 ) by A9, FUNCT_1:9;
A11: [x1,x0] in the InternalRel of R by A9, A10, WELLORD1:def 1;
reconsider x1 = x1 as Element of R by A10;
A12: ( (F1 | (the InternalRel of R -Seg x0)) . x1 = F1 . x1 & (F2 | (the InternalRel of R -Seg x0)) . x1 = F2 . x1 ) by A9, A10, FUNCT_1:72;
x1 <> x0 by A9, A10, WELLORD1:def 1;
hence contradiction by A8, A10, A11, A12; :: thesis: verum

end;

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