:: deftheorem Def53 defines array-correct AOFA_A00:def 53 :
for n being Nat
for B being BoolSignature holds
( B is n array-correct iff the ResultSort of B . ( the connectives of B . (n + 1)) <> the bool-sort of B );