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

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