for U1 being Universal_Algebra
for o being OperSymbol of (MSSign U1)
for y being Element of Args (o,(MSAlg U1)) holds y is FinSequence of the carrier of U1