for S being non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature
for I being integer SortSymbol of S
for A being non-empty bool-correct 4,1 integer 11,1,1 -array MSAlgebra over S holds
( the Sorts of A . (the_array_sort_of S) = INT ^omega & ( for i, j being Element of A,I st i is non negative Integer holds
init.array (i,j) = (Segm i) --> j ) & ( for a being Element of the Sorts of A . (the_array_sort_of S) holds
( length (a,I) = card a & ( for i being Element of A,I
for f being Function st f = a & i in dom f holds
( a . i = f . i & ( for x being Element of A,I holds (a,i) <- x = f +* (i,x) ) ) ) ) ) )