:: deftheorem Def21 defines pi MSAFREE:def 21 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for o being OperSymbol of S
for p being FinSequence st p in Args (o,U0) holds
pi (o,U0,p) = (Den (o,U0)) . p;