:: deftheorem Def10 defines FuncComp ALTCAT_1:def 10 :
for A, B being functional set
for b₃ being compositional ManySortedFunction of [:B,A:] holds
( b₃ = FuncComp (A,B) iff verum );