:: deftheorem defines . AOFA_A01:def 16 :
for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature
for X being V3() ManySortedSet of the carrier of S
for T being non-empty b₂,b₁ -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for M being pure Element of the generators of G . (the_array_sort_of S)
for i being Integer holds M . (i,I) = (@ M) . (^ (i,T,I));