let S be 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 ) )
let J0, L0 be set ; for K being SortSymbol of S st the connectives of S . 11 is_of_type <*J0,L0*>,K holds
( J0 = the_array_sort_of S & ( for I being integer SortSymbol of S holds the_array_sort_of S <> I ) )
let K0 be SortSymbol of S; ( the connectives of S . 11 is_of_type <*J0,L0*>,K0 implies ( J0 = the_array_sort_of S & ( for I being integer SortSymbol of S holds the_array_sort_of S <> I ) ) )
assume A1:
the connectives of S . 11 is_of_type <*J0,L0*>,K0
; ( J0 = the_array_sort_of S & ( for I being integer SortSymbol of S holds the_array_sort_of S <> I ) )
consider J, K, L being Element of S such that
A2:
( L = 1 & K = 1 & J <> L & J <> K & the connectives of S . 11 is_of_type <*J,K*>,L & the connectives of S . (11 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (11 + 2) is_of_type <*J*>,K & the connectives of S . (11 + 3) is_of_type <*K,L*>,J )
by AOFA_A00:def 51;
A3:
the_array_sort_of S = J
by A2;
thus J0 =
<*J0,L0*> . 1
by FINSEQ_1:44
.=
( the Arity of S . ( the connectives of S . 11)) . 1
by A1
.=
<*J,K*> . 1
by A2
.=
the_array_sort_of S
by A3, FINSEQ_1:44
; for I being integer SortSymbol of S holds the_array_sort_of S <> I
thus
for I being integer SortSymbol of S holds the_array_sort_of S <> I
by A2, AOFA_A00:def 40; verum