:: deftheorem defines := AOFA_A00:def 17 :
for J being non empty non void ManySortedSign
for T being non-empty MSAlgebra over J
for X being V2() GeneratorSet of T
for A being non empty ProgramAlgStr over J,T,X
for a being SortSymbol of J
for x being Element of X . a
for t being Element of T,a holds x := (t,A) = the assignments of A . [x,t];