theorem Th22: :: MSATERM:22

for S being non empty non void ManySortedSign
for V being non-empty ManySortedSet of the carrier of S
for o being OperSymbol of S
for a being ArgumentSeq of Sym (o,V) holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
a . i is Term of S,V ) )