theorem Th16: :: CIRCCOMB:16

for S1 being non empty non void ManySortedSign
for S2 being non empty ManySortedSign st S1 tolerates S2 holds
for o1 being OperSymbol of S1
for o being OperSymbol of (S1 +* S2) st o1 = o holds
( the_arity_of o = the_arity_of o1 & the_result_sort_of o = the_result_sort_of o1 )