ex f being Function st ( dom f = F1() & ( for x being element st x in F1() holds ex n being Nat st ( f . x = n & P1[x,n] & ( for m being Nat st P1[x,m] holds n <= m ) ) ) )
provided
A1:
for x being element st x in F1() holds ex n being Nat st P1[x,n]
ex T being DecoratedTree of F1() st ( T .{}= F2() & ( for t being Element of dom T holds ( succ t = { (t ^<*k*>) where k is Nat : k in F3((T . t)) } & ( for n being Nat st n in F3((T . t)) holds T .(t ^<*n*>)= F4() . ((T . t),n) ) ) ) )
provided
A1:
for d being Element of F1() for k1, k2 being Nat st k1 <= k2 & k2 in F3(d) holds k1 in F3(d)
ex T being DecoratedTree of F1() st ( T .{}= F2() & ( for t being Element of dom T holds ( succ t = { (t ^<*k*>) where k is Nat : k < F3((T . t)) } & ( for n being Nat st n < F3((T . t)) holds T .(t ^<*n*>)= F4() . ((T . t),n) ) ) ) )
ex T being DecoratedTree of F1() st ( T .{}= F2() & ( for t being Element of dom T holds ( succ t = { (t ^<*k*>) where k is Nat : P1[k,T . t] } & ( for n being Nat st P1[n,T . t] holds T .(t ^<*n*>)= F3() . ((T . t),n) ) ) ) )
provided
A1:
for d being Element of F1() for k1, k2 being Nat st k1 <= k2 & P1[k2,d] holds P1[k1,d]