:: deftheorem Def13 defines ** AOFA_I00:def 13 :
for N being set
for v, f, b₄ being Function holds
( b₄ = v ** (f,N) iff ( ex Y being set st
( ( for y being set holds
( y in Y iff ex h being Function st
( h in dom v & y in rng h ) ) ) & ( for a being set holds
( a in dom b₄ iff ( a in Funcs (N,Y) & ex g being Function st
( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b₄ holds
b₄ . g = v . (g * f) ) ) );