let j, k be set ; :: thesis:
let i, m, n be Nat; :: thesis:
assume A1: m >= 4 ; :: thesis:
assume A2: ( m + 6 <= n & i >= 1 ) ; :: thesis:
let S be non empty non void 1-1-connectives bool-correct BoolSignature ; :: thesis:
assume A3: len the connectives of S >= (n + i) + 3 ; :: according to AOFA_A00:def 50 :: thesis:
given J, K, L being Element of S such that A4: ( L = j & K = k & J <> L & J <> K & the connectives of S . (n + i) is_of_type <*J,K*>,L & the connectives of S . ((n + i) + 1) is_of_type <*J,K,L*>,J & the connectives of S . ((n + i) + 2) is_of_type <*J*>,K & the connectives of S . ((n + i) + 3) is_of_type <*K,L*>,J ) ; :: thesis:
A5: S is i + n,j,k -array by A3, A4;
assume A6: len the connectives of S >= m + 6 ; :: according to AOFA_A00:def 38 :: thesis:
given I being Element of S such that A7: ( I = k & I <> the bool-sort of S & the connectives of S . m is_of_type {} ,I & the connectives of S . (m + 1) is_of_type {} ,I & the connectives of S . m <> the connectives of S . (m + 1) & the connectives of S . (m + 2) is_of_type <*I*>,I & the connectives of S . (m + 3) is_of_type <*I,I*>,I & the connectives of S . (m + 4) is_of_type <*I,I*>,I & the connectives of S . (m + 5) is_of_type <*I,I*>,I & the connectives of S . (m + 3) <> the connectives of S . (m + 4) & the connectives of S . (m + 3) <> the connectives of S . (m + 5) & the connectives of S . (m + 4) <> the connectives of S . (m + 5) & the connectives of S . (m + 6) is_of_type <*I,I*>, the bool-sort of S ) ; :: thesis:
A8: S is m,k integer by A6, A7;
set r = the connectives of S /^ n;
set W = rng ( the connectives of S /^ n);
A9: ( (n + i) + 3 = n + (i + 3) & n <= n + (i + 3) ) by NAT_1:12;
then A10: len the connectives of S >= n by A3, XXREAL_0:2;
then len ( the connectives of S /^ n) = (len the connectives of S) - n by RFINSEQ:def 1;
then A11: len ( the connectives of S /^ n) >= (n + (i + 3)) - n by A3, XREAL_1:9;
then ( len ( the connectives of S /^ n) >= i + 3 & (i + 1) + 2 >= 2 ) by NAT_1:11;
then len ( the connectives of S /^ n) >= 2 by XXREAL_0:2;
then the connectives of S /^ n <> {} ;
then reconsider W = rng ( the connectives of S /^ n) as non empty set ;
set O = the carrier' of S \ W;
m <= m + 6 by NAT_1:11;
then m <= n by A2, XXREAL_0:2;
then A12: 4 <= n by A1, XXREAL_0:2;
then A13: ( 1 <= n & 1 <= m ) by A1, XXREAL_0:2;
n <= n + (i + 3) by NAT_1:11;
then 1 <= (n + i) + 3 by A13, XXREAL_0:2;
then 1 <= len the connectives of S by A3, XXREAL_0:2;
then A14: 1 in dom the connectives of S by FINSEQ_3:25;
then A15: the connectives of S . 1 in the carrier' of S by FUNCT_1:102;

now :: thesis:

assume the connectives of S . 1 in W ; :: thesis:
then consider x being object such that
A16: ( x in dom ( the connectives of S /^ n) & the connectives of S . 1 = ( the connectives of S /^ n) . x ) by FUNCT_1:def 3;
reconsider x = x as Nat by A16;
( ( the connectives of S /^ n) . x = the connectives of S . (x + n) & n + x in dom the connectives of S ) by A10, A16, RFINSEQ:def 1, FINSEQ_5:26;
then ( 1 = n + x & n = n + 0 ) by A14, A16, FUNCT_1:def 4;
then x = 0 by A13, XREAL_1:6, NAT_1:3;
hence contradiction by A16, FINSEQ_3:24; :: thesis:

end;

then reconsider O = the carrier' of S \ W as non empty set by A15, XBOOLE_0:def 5;
A17: W c= the carrier' of S by FINSEQ_1:def 4;
reconsider A = the Arity of S | O as Function of O,( the carrier of S *) by FUNCT_2:32;
reconsider Ac = the Arity of S | W as Function of W,( the carrier of S *) by A17, FUNCT_2:32;
reconsider R = the ResultSort of S | O as Function of O, the carrier of S by FUNCT_2:32;
reconsider Rc = the ResultSort of S | W as Function of W, the carrier of S by A17, FUNCT_2:32;
set s = the bool-sort of S;
set p = the connectives of S | n;
rng ( the connectives of S | n) c= O

proof

end;

then reconsider c = the connectives of S | n as FinSequence of O by FINSEQ_1:def 4;
reconsider cc = the connectives of S /^ n as FinSequence of W by FINSEQ_1:def 4;
set B = BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #);
set C = ConnectivesSignature(# the carrier of S,W,Ac,Rc,cc #);

now :: thesis:

end;

then reconsider B = BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) as non empty non void bool-correct BoolSignature by Th60;
reconsider C = ConnectivesSignature(# the carrier of S,W,Ac,Rc,cc #) as non empty non void ConnectivesSignature ;
take B ; :: thesis:
take C ; :: thesis:
A26: the carrier of S = the carrier of B \/ the carrier of C ;
A27: the carrier' of S = the carrier' of B \/ the carrier' of C by FINSEQ_1:def 4, XBOOLE_1:45;
dom the Arity of S = the carrier' of S by FUNCT_2:def 1;
then A28: the Arity of S = the Arity of B +* the Arity of C by A27, FUNCT_4:70;
dom the ResultSort of S = the carrier' of S by FUNCT_2:def 1;
then the ResultSort of S = the ResultSort of B +* the ResultSort of C by A27, FUNCT_4:70;
then A29: ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = B +* C by A26, A27, A28, CIRCCOMB:def 2;
the connectives of S = c ^ cc by RFINSEQ:8;
hence BoolSignature(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S, the bool-sort of S, the connectives of S #) = B +* C by A29, Def52; :: thesis:
thus A30: len the connectives of B = n by A9, A3, XXREAL_0:2, FINSEQ_1:59; :: according to AOFA_A00:def 29 :: thesis:

now :: thesis:

end;

hence B is m,k integer by A8, Th61; :: thesis:

now :: thesis:

thus len the connectives of C >= i + 3 by A11; :: thesis:
thus 1 <= i by A2; :: thesis:
let z be Nat; :: thesis:
assume ( z >= i & z <= i + 3 ) ; :: thesis:
then ( 1 <= z & z <= len ( the connectives of S /^ n) ) by A11, A2, XXREAL_0:2;
then z in dom ( the connectives of S /^ n) by FINSEQ_3:25;
then A32: ( the connectives of C . z in W & the connectives of C . z = the connectives of S . (z + n) ) by A10, FUNCT_1:102, RFINSEQ:def 1;
thus the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) by A32, FUNCT_1:49; :: thesis:
thus the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) by A32, FUNCT_1:49; :: thesis:

end;

hence C is i,j,k -array by A5, Th62; :: thesis:
thus ( the carrier of B = the carrier of C & the carrier' of B = the carrier' of S \ (rng the connectives of C) & the carrier' of C = rng the connectives of C & the connectives of B = the connectives of S | n & the connectives of C = the connectives of S /^ n ) ; :: thesis: