:: deftheorem Def54 defines with_an_operation_for_each_sort ABCMIZ_1:def 54 :
for S being ManySortedSign holds
( S is with_an_operation_for_each_sort iff the carrier of S c= rng the ResultSort of S );