let S be non empty non void 11,1,1 -array BoolSignature ; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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
.= ( the Arity of S . ( the connectives of S . 11)) . 1 by A1
.= <*J,K*> . 1 by A2
.= the_array_sort_of S by A3 ; :: thesis: 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; :: thesis: verum