:: deftheorem defines -array AOFA_A00:def 51 :
for S being non empty non void ConnectivesSignature
for I, N being set
for n being Nat
for A being MSAlgebra over S holds
( A is n,I,N -array iff ex J, K being Element of S st
( K = I & the connectives of S . n is_of_type <*J,N*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . N = INT & ( for a being finite 0 -based array of the Sorts of A . K holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. n),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. (n + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (n + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,K st i >= 0 holds
(Den (( the connectives of S /. (n + 3)),A)) . <*i,x*> = (Segm i) --> x ) ) );