theorem Th5: :: AOFA_L00:5

for x being object
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for s, r being SortSymbol of S
for T being MSAlgebra over S st o is_of_type <*s*>,r & x in the Sorts of T . s holds
<*x*> in Args (o,T)