:: deftheorem Def9 defines Funcs FUNCTOR2:def 9 :
for I being set
for A, B being ManySortedSet of I
for b₄ being set holds
( ( ( for i being set st i in I & B . i = {} holds
A . i = {} ) implies ( b₄ = Funcs (A,B) iff for x being set holds
( x in b₄ iff x is ManySortedFunction of A,B ) ) ) & ( ex i being set st
( i in I & B . i = {} & not A . i = {} ) implies ( b₄ = Funcs (A,B) iff b₄ = {} ) ) );