:: deftheorem Def18 defines -States AOFA_A00:def 18 :
for J being non empty non void ManySortedSign
for T, C being non-empty MSAlgebra over J
for X being V2() GeneratorSet of T
for b₅ being Subset of (MSFuncs (X, the Sorts of C)) holds
( b₅ = C -States X iff for s being ManySortedFunction of X, the Sorts of C holds
( s in b₅ iff ex f being ManySortedFunction of T,C st
( f is_homomorphism T,C & s = f || X ) ) );