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 S1[ 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: 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 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 ;
dom (F2 | ( the InternalRel of R -Seg x0)) = the InternalRel of R -Seg x0 by ;
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 ;
A14: [x1,x0] in the InternalRel of R by ;
reconsider x1 = x1 as Element of R by A12;
A15: x1 <> x0 by ;
( (F1 | ( the InternalRel of R -Seg x0)) . x1 = F1 . x1 & (F2 | ( the InternalRel of R -Seg x0)) . x1 = F2 . x1 ) by ;
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