theorem :: MSAFREE2:12

for S being non empty non void ManySortedSign
for X being non-empty ManySortedSet of the carrier of S
for v being Vertex of S
for o being OperSymbol of S
for e being Element of the Sorts of (FreeMSA X) . v st e . {} = [o, the carrier of S] holds
ex p being DTree-yielding FinSequence st
( len p = len (the_arity_of o) & ( for i being Nat st i in dom p holds
p . i in the Sorts of (FreeMSA X) . ((the_arity_of o) . i) ) )