:: deftheorem defines -States AOFA_A00:def 19 :
for B being non empty non void ManySortedSign
for T, C being non-empty MSAlgebra over B
for X being V2() GeneratorSet of T
for a being SortSymbol of B
for x being Element of X . a
for f being Element of C,a
for b₈ being Subset of (C -States X) holds
( b₈ = f -States (X,x) iff for s being ManySortedFunction of X, the Sorts of C holds
( s in b₈ iff ( s in C -States X & (s . a) . x <> f ) ) );