theorem Th71: :: AOFA_A01:71

for S being non empty non void 11,1,1 -array BoolSignature
for J, L being set
for K being SortSymbol of S st the connectives of S . 11 is_of_type <*J,L*>,K holds
( J = the_array_sort_of S & ( for I being integer SortSymbol of S holds the_array_sort_of S <> I ) )