theorem Th6: :: AOFA_L00:6

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