let M be Element of the Sorts of A . (the_array_sort_of S); :: thesis: ( M is Relation-like & M is Function-like )
set I = the integer SortSymbol of S;
consider J, K being Element of S such that
A1: ( K = 1 & the connectives of S . 11 is_of_type <*J,1*>,K & the Sorts of A . J = ( the Sorts of A . K) ^omega & the Sorts of A . 1 = INT & ( for a being finite 0 -based array of the Sorts of A . K holds
( ( for i being Integer st i in dom a holds
( (Den (( the connectives of S /. 11),A)) . <*a,i*> = a . i & ( for x being Element of A,K holds (Den (( the connectives of S /. (11 + 1)),A)) . <*a,i,x*> = a +* (i,x) ) ) ) & (Den (( the connectives of S /. (11 + 2)),A)) . <*a*> = card a ) ) & ( for i being Integer
for x being Element of A,K st i >= 0 holds
(Den (( the connectives of S /. (11 + 3)),A)) . <*i,x*> = (Segm i) --> x ) ) by AOFA_A00:def 52;
J = the_array_sort_of S by A1, Th71;
hence ( M is Relation-like & M is Function-like ) by A1; :: thesis: verum