theorem Th8: :: MSUALG_1:8
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))