let S be non empty non void bool-correct 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: for I being integer SortSymbol of S holds
( the_array_sort_of S <> I & the connectives of S . 11 is_of_type <*(the_array_sort_of S),I*>,I & the connectives of S . (11 + 1) is_of_type <*(the_array_sort_of S),I,I*>, the_array_sort_of S & the connectives of S . (11 + 2) is_of_type <*(the_array_sort_of S)*>,I & the connectives of S . (11 + 3) is_of_type <*I,I*>, the_array_sort_of S )
let I be integer SortSymbol of S; :: thesis: ( the_array_sort_of S <> I & the connectives of S . 11 is_of_type <*(the_array_sort_of S),I*>,I & the connectives of S . (11 + 1) is_of_type <*(the_array_sort_of S),I,I*>, the_array_sort_of S & the connectives of S . (11 + 2) is_of_type <*(the_array_sort_of S)*>,I & the connectives of S . (11 + 3) is_of_type <*I,I*>, the_array_sort_of S )
consider J, K, L being Element of S such that
A1: ( 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;
( the_array_sort_of S = J & I = 1 ) by A1, AOFA_A00:def 40;
hence ( the_array_sort_of S <> I & the connectives of S . 11 is_of_type <*(the_array_sort_of S),I*>,I & the connectives of S . (11 + 1) is_of_type <*(the_array_sort_of S),I,I*>, the_array_sort_of S & the connectives of S . (11 + 2) is_of_type <*(the_array_sort_of S)*>,I & the connectives of S . (11 + 3) is_of_type <*I,I*>, the_array_sort_of S ) by A1; :: thesis: verum