theorem Th14: :: CIRCCOMB:14

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