:: deftheorem defines @ AOFA_A01:def 7 :
for S being non empty non void ManySortedSign
for T being non-empty MSAlgebra over S
for G being V3() GeneratorSet of T
for s being SortSymbol of S
for x being Element of G . s holds @ x = x;