:: deftheorem defines is_recursively_expressed_by WELLFND1:def 5 :
for R being non empty RelStr
for V being non empty set
for H being Function of [: the carrier of R,(PFuncs ( the carrier of R,V)):],V
for F being Function holds
( F is_recursively_expressed_by H iff for x being Element of R holds F . x = H . (x,(F | ( the InternalRel of R -Seg x))) );