let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; for I being integer SortSymbol of S
for o being OperSymbol of S st o = In (( the connectives of S . 12), the carrier' of S) holds
( the_arity_of o = <*(the_array_sort_of S),I,I*> & the_result_sort_of o = the_array_sort_of S )
let I be integer SortSymbol of S; for o being OperSymbol of S st o = In (( the connectives of S . 12), the carrier' of S) holds
( the_arity_of o = <*(the_array_sort_of S),I,I*> & the_result_sort_of o = the_array_sort_of S )
let o be OperSymbol of S; ( o = In (( the connectives of S . 12), the carrier' of S) implies ( the_arity_of o = <*(the_array_sort_of S),I,I*> & the_result_sort_of o = the_array_sort_of S ) )
assume A1:
o = In (( the connectives of S . 12), the carrier' of S)
; ( the_arity_of o = <*(the_array_sort_of S),I,I*> & the_result_sort_of o = the_array_sort_of S )
11 + 3 <= len the connectives of S
by AOFA_A00:def 51;
then
12 <= len the connectives of S
by XXREAL_0:2;
then
12 in dom the connectives of S
by FINSEQ_3:25;
then
o = the connectives of S . 12
by A1, FUNCT_1:102, SUBSET_1:def 8;
then
o is_of_type <*(the_array_sort_of S),I,I*>, the_array_sort_of S
by Th73;
hence
( the_arity_of o = <*(the_array_sort_of S),I,I*> & the_result_sort_of o = the_array_sort_of S )
; verum