set Y = {I,N};
set V = (I,N) --> (INT,INT);
consider J, K, L being Element of S such that
A1: ( L = I & K = N & J <> L & J <> K & the connectives of S . 1 is_of_type <*J,K*>,L & the connectives of S . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of S . (1 + 2) is_of_type <*J*>,K & the connectives of S . (1 + 3) is_of_type <*K,L*>,J ) by Def50;
A2: the ResultSort of S . ( the connectives of S . 2) nin {I,N} by A1, TARSKI:def 2;
( dom ((I,N) --> (INT,INT)) = {I,N} & (I,N) --> (INT,INT) = (I .--> INT) +* (N .--> INT) ) by FUNCT_4:62, FUNCT_4:def 4;
then reconsider V = (I,N) --> (INT,INT) as V2() ManySortedSet of {I,N} by RELAT_1:def 18, PARTFUN1:def 2;
( V . N = INT & I in {I,N} ) by TARSKI:def 2, FUNCT_4:63;
then consider A being strict non-empty MSAlgebra over S such that
A3: ( A is 1,I,N -array & the Sorts of A tolerates V ) by A2, Th56;
take A ; :: thesis: A is 1,I,N -array
thus A is 1,I,N -array by A3; :: thesis: verum