:: deftheorem Def18 defines .. PRALG_1:def 20 :
for I being set
for f being ManySortedFunction of I
for x being ManySortedSet of I
for b₄ being Function holds
( b₄ = f .. x iff ( dom b₄ = I & ( for i being set st i in I holds
for g being Function st g = f . i holds
b₄ . i = g . (x . i) ) ) );