let M, O, N, I be set ; :: thesis:
assume A1: ( I in M & N in M ) ; :: thesis:
set X = succ M;
set Y = {O,(succ O),(succ (succ O)),(succ (succ (succ O)))};
reconsider o0 = O, o1 = succ O, o2 = succ (succ O), o3 = succ (succ (succ O)) as Element of {O,(succ O),(succ (succ O)),(succ (succ (succ O)))} by ENUMSET1:def 2;
reconsider m = M, i = I, n = N as Element of succ M by A1, XBOOLE_0:def 3, ORDINAL1:6;
set A = (o0,o1,o2,o3) --> (<*m,n*>,<*m,n,i*>,<*m*>,<*n,i*>);
A3: ( o0 in o1 & o1 in o2 & o2 in o3 ) by ORDINAL1:6;
then A4: o0,o1,o2,o3 are_mutually_distinct by XREGULAR:7;
then ( rng ((o0,o1,o2,o3) --> (<*m,n*>,<*m,n,i*>,<*m*>,<*n,i*>)) = {<*m,n*>,<*m,n,i*>,<*m*>,<*n,i*>} & <*m,n*> in (succ M) * & <*m,n,i*> in (succ M) * & <*m*> in (succ M) * & <*n,i*> in (succ M) * ) by FUNCT_4:143, FINSEQ_1:def 11;
then ( dom ((o0,o1,o2,o3) --> (<*m,n*>,<*m,n,i*>,<*m*>,<*n,i*>)) = {O,(succ O),(succ (succ O)),(succ (succ (succ O)))} & rng ((o0,o1,o2,o3) --> (<*m,n*>,<*m,n,i*>,<*m*>,<*n,i*>)) c= (succ M) * ) by FUNCT_4:137, QUATERNI:5;
then reconsider A = (o0,o1,o2,o3) --> (<*m,n*>,<*m,n,i*>,<*m*>,<*n,i*>) as Function of {O,(succ O),(succ (succ O)),(succ (succ (succ O)))},((succ M) *) by FUNCT_2:2;
set R = (o0,o1,o2,o3) --> (i,m,n,m);
rng ((o0,o1,o2,o3) --> (i,m,n,m)) = {i,m,n,m} by A4, FUNCT_4:143;
then ( dom ((o0,o1,o2,o3) --> (i,m,n,m)) = {O,(succ O),(succ (succ O)),(succ (succ (succ O)))} & rng ((o0,o1,o2,o3) --> (i,m,n,m)) c= succ M ) by FUNCT_4:137, QUATERNI:5;
then reconsider R = (o0,o1,o2,o3) --> (i,m,n,m) as Function of {O,(succ O),(succ (succ O)),(succ (succ (succ O)))},(succ M) by FUNCT_2:2;
set c = <*o0,o1,o2,o3*>;
set C = ConnectivesSignature(# (succ M),{O,(succ O),(succ (succ O)),(succ (succ (succ O)))},A,R,<*o0,o1,o2,o3*> #);
ConnectivesSignature(# (succ M),{O,(succ O),(succ (succ O)),(succ (succ (succ O)))},A,R,<*o0,o1,o2,o3*> #) is 4 -connectives by CARD_1:def 7;
then reconsider C = ConnectivesSignature(# (succ M),{O,(succ O),(succ (succ O)),(succ (succ (succ O)))},A,R,<*o0,o1,o2,o3*> #) as non empty non void strict 4 -connectives ConnectivesSignature ;
take C ; :: thesis:
thus C is 1,I,N -array :: thesis:

proof

thus len the connectives of C >= 1 + 3 by CARD_1:def 7; :: according to AOFA_A00:def 50 :: thesis:
reconsider K = n, L = i, J = m as Element of C ;
take J ; :: thesis:
take K ; :: thesis:
take L ; :: thesis:
thus ( L = I & K = N ) ; :: thesis:
thus ( J <> L & J <> K ) by A1; :: thesis:
( <*o0,o1,o2,o3*> . 1 = o0 & o0 <> o1 & o0 <> o2 & o0 <> o3 ) by A3, FINSEQ_4:76, XREGULAR:7;
hence ( the Arity of C . ( the connectives of C . 1) = <*J,K*> & the ResultSort of C . ( the connectives of C . 1) = L ) by FUNCT_4:142; :: according to AOFA_A00:def 8 :: thesis:
( <*o0,o1,o2,o3*> . 2 = o1 & o2 <> o1 & o1 <> o3 ) by A3, FINSEQ_4:76;
hence ( the Arity of C . ( the connectives of C . (1 + 1)) = <*J,K,L*> & the ResultSort of C . ( the connectives of C . (1 + 1)) = J ) by FUNCT_4:141; :: according to AOFA_A00:def 8 :: thesis:
( <*o0,o1,o2,o3*> . 3 = o2 & o2 <> o3 ) by A3, FINSEQ_4:76;
hence ( the Arity of C . ( the connectives of C . (1 + 2)) = <*J*> & the ResultSort of C . ( the connectives of C . (1 + 2)) = K ) by FUNCT_4:140; :: according to AOFA_A00:def 8 :: thesis:
<*o0,o1,o2,o3*> . 4 = o3 by FINSEQ_4:76;
hence ( the Arity of C . ( the connectives of C . (1 + 3)) = <*K,L*> & the ResultSort of C . ( the connectives of C . (1 + 3)) = J ) by FUNCT_4:139; :: according to AOFA_A00:def 8 :: thesis:

end;

thus the connectives of C is one-to-one by A4, Th14; :: according to AOFA_A00:def 28 :: thesis:
thus M c= the carrier of C by XBOOLE_1:7; :: thesis:

now :: thesis:

given x being object such that A5: ( x in O & x in the carrier' of C ) ; :: thesis:
( x = o0 or x = o1 or x = o2 or x = o3 ) by A5, ENUMSET1:def 2;
hence contradiction by A5, A3, XREGULAR:7, XREGULAR:8; :: thesis:

end;

hence O misses the carrier' of C by XBOOLE_0:3; :: thesis:
( <*o0,o1,o2,o3*> . 2 = o1 & o2 <> o1 & o1 <> o3 ) by A3, FINSEQ_4:76;
then A: the ResultSort of C . ( the connectives of C . (1 + 1)) = m by FUNCT_4:141;
reconsider nn = the ResultSort of C . ( the connectives of C . 2) as set ;
not nn in nn ;
hence the ResultSort of C . ( the connectives of C . 2) nin M by A; :: thesis: