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_{1}[ 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_{1}[x]
by A4;

consider x0 being Element of R such that

A7: S_{1}[x0]
and

A8: for y being Element of R holds

( not x0 <> y or not S_{1}[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)

.= F2 . x0 by A2 ;

hence contradiction by A7; :: thesis: verum

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

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

consider x0 being Element of R such that

A7: S

A8: for y being Element of R holds

( not x0 <> y or not S

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

then F1 . x0 =
H . (x0,(F2 | ( the InternalRel of R -Seg x0)))
by A1
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;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

.= F2 . x0 by A2 ;

hence contradiction by A7; :: thesis: verum