let M, O, N, I be set ; :: thesis: ( I in M & N in M implies ex C being non empty non void strict 4 -connectives ConnectivesSignature st

( C is 1,I,N -array & C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M ) )

assume A1: ( I in M & N in M ) ; :: thesis: ex C being non empty non void strict 4 -connectives ConnectivesSignature st

( C is 1,I,N -array & C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )

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: ( C is 1,I,N -array & C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )

thus C is 1,I,N -array :: thesis: ( C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )

thus M c= the carrier of C by XBOOLE_1:7; :: thesis: ( O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )

( <*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: verum

( C is 1,I,N -array & C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M ) )

assume A1: ( I in M & N in M ) ; :: thesis: ex C being non empty non void strict 4 -connectives ConnectivesSignature st

( C is 1,I,N -array & C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )

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: ( C is 1,I,N -array & C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )

thus C is 1,I,N -array :: thesis: ( C is 1-1-connectives & M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )

proof

thus
the connectives of C is one-to-one
by A4, Th14; :: according to AOFA_A00:def 28 :: thesis: ( M c= the carrier of C & O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )
thus
len the connectives of C >= 1 + 3
by CARD_1:def 7; :: according to AOFA_A00:def 50 :: thesis: ex J, K, L being Element of C st

( L = I & K = N & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

reconsider K = n, L = i, J = m as Element of C ;

take J ; :: thesis: ex K, L being Element of C st

( L = I & K = N & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

take K ; :: thesis: ex L being Element of C st

( L = I & K = N & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

take L ; :: thesis: ( L = I & K = N & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

thus ( L = I & K = N ) ; :: thesis: ( J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

thus ( J <> L & J <> K ) by A1; :: thesis: ( the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

( <*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: ( the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

( <*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: ( the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

( <*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: the connectives of C . (1 + 3) is_of_type <*K,L*>,J

<*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: verum

end;( L = I & K = N & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

reconsider K = n, L = i, J = m as Element of C ;

take J ; :: thesis: ex K, L being Element of C st

( L = I & K = N & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

take K ; :: thesis: ex L being Element of C st

( L = I & K = N & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

take L ; :: thesis: ( L = I & K = N & J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

thus ( L = I & K = N ) ; :: thesis: ( J <> L & J <> K & the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

thus ( J <> L & J <> K ) by A1; :: thesis: ( the connectives of C . 1 is_of_type <*J,K*>,L & the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

( <*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: ( the connectives of C . (1 + 1) is_of_type <*J,K,L*>,J & the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

( <*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: ( the connectives of C . (1 + 2) is_of_type <*J*>,K & the connectives of C . (1 + 3) is_of_type <*K,L*>,J )

( <*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: the connectives of C . (1 + 3) is_of_type <*K,L*>,J

<*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: verum

thus M c= the carrier of C by XBOOLE_1:7; :: thesis: ( O misses the carrier' of C & the ResultSort of C . ( the connectives of C . 2) nin M )

now :: thesis: for x being object holds

( not x in O or not x in the carrier' of C )

hence
O misses the carrier' of C
by XBOOLE_0:3; :: thesis: the ResultSort of C . ( the connectives of C . 2) nin M( not x in O or not x in the carrier' of C )

given x being object such that A5:
( x in O & x in the carrier' of C )
; :: thesis: contradiction

( 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: verum

end;( 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: verum

( <*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: verum