let j, k be set ; :: thesis: for i, m, n being Nat st m >= 4 & m + 6 <= n & i >= 1 holds

for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds

ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

let i, m, n be Nat; :: thesis: ( m >= 4 & m + 6 <= n & i >= 1 implies for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds

ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

assume A1: m >= 4 ; :: thesis: ( not m + 6 <= n or not i >= 1 or for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds

ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

assume A2: ( m + 6 <= n & i >= 1 ) ; :: thesis: for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds

ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

let S be non empty non void 1-1-connectives bool-correct BoolSignature ; :: thesis: ( S is n + i,j,k -array & S is m,k integer implies ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

assume A3: len the connectives of S >= (n + i) + 3 ; :: according to AOFA_A00:def 50 :: thesis: ( for J, K, L being Element of S holds

( not L = j or not K = k or not J <> L or not J <> K or not the connectives of S . (n + i) is_of_type <*J,K*>,L or not the connectives of S . ((n + i) + 1) is_of_type <*J,K,L*>,J or not the connectives of S . ((n + i) + 2) is_of_type <*J*>,K or not the connectives of S . ((n + i) + 3) is_of_type <*K,L*>,J ) or not S is m,k integer or ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

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: ( not S is m,k integer or ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

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: ( for I being Element of S holds

( not I = k or not I <> the bool-sort of S or not the connectives of S . m is_of_type {} ,I or not the connectives of S . (m + 1) is_of_type {} ,I or not the connectives of S . m <> the connectives of S . (m + 1) or not the connectives of S . (m + 2) is_of_type <*I*>,I or not the connectives of S . (m + 3) is_of_type <*I,I*>,I or not the connectives of S . (m + 4) is_of_type <*I,I*>,I or not the connectives of S . (m + 5) is_of_type <*I,I*>,I or not the connectives of S . (m + 3) <> the connectives of S . (m + 4) or not the connectives of S . (m + 3) <> the connectives of S . (m + 5) or not the connectives of S . (m + 4) <> the connectives of S . (m + 5) or not the connectives of S . (m + 6) is_of_type <*I,I*>, the bool-sort of S ) or ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

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: ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

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;

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

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 #);

reconsider C = ConnectivesSignature(# the carrier of S,W,Ac,Rc,cc #) as non empty non void ConnectivesSignature ;

take B ; :: thesis: ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

take C ; :: thesis: ( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

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: ( B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

thus A30: len the connectives of B = n by A9, A3, XXREAL_0:2, FINSEQ_1:59; :: according to AOFA_A00:def 29 :: thesis: ( B is m,k integer & C is i,j,k -array & 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 )

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

for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds

ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

let i, m, n be Nat; :: thesis: ( m >= 4 & m + 6 <= n & i >= 1 implies for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds

ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

assume A1: m >= 4 ; :: thesis: ( not m + 6 <= n or not i >= 1 or for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds

ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

assume A2: ( m + 6 <= n & i >= 1 ) ; :: thesis: for S being non empty non void 1-1-connectives bool-correct BoolSignature st S is n + i,j,k -array & S is m,k integer holds

ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

let S be non empty non void 1-1-connectives bool-correct BoolSignature ; :: thesis: ( S is n + i,j,k -array & S is m,k integer implies ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

assume A3: len the connectives of S >= (n + i) + 3 ; :: according to AOFA_A00:def 50 :: thesis: ( for J, K, L being Element of S holds

( not L = j or not K = k or not J <> L or not J <> K or not the connectives of S . (n + i) is_of_type <*J,K*>,L or not the connectives of S . ((n + i) + 1) is_of_type <*J,K,L*>,J or not the connectives of S . ((n + i) + 2) is_of_type <*J*>,K or not the connectives of S . ((n + i) + 3) is_of_type <*K,L*>,J ) or not S is m,k integer or ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

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: ( not S is m,k integer or ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

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: ( for I being Element of S holds

( not I = k or not I <> the bool-sort of S or not the connectives of S . m is_of_type {} ,I or not the connectives of S . (m + 1) is_of_type {} ,I or not the connectives of S . m <> the connectives of S . (m + 1) or not the connectives of S . (m + 2) is_of_type <*I*>,I or not the connectives of S . (m + 3) is_of_type <*I,I*>,I or not the connectives of S . (m + 4) is_of_type <*I,I*>,I or not the connectives of S . (m + 5) is_of_type <*I,I*>,I or not the connectives of S . (m + 3) <> the connectives of S . (m + 4) or not the connectives of S . (m + 3) <> the connectives of S . (m + 5) or not the connectives of S . (m + 4) <> the connectives of S . (m + 5) or not the connectives of S . (m + 6) is_of_type <*I,I*>, the bool-sort of S ) or ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 ) )

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: ex B being non empty non void bool-correct BoolSignature ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

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: not the connectives of S . 1 in W

then reconsider O = the carrier' of S \ W as non empty set by A15, XBOOLE_0:def 5;assume
the connectives of S . 1 in W
; :: thesis: contradiction

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

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

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

then reconsider c = the connectives of S | n as FinSequence of O by FINSEQ_1:def 4;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng ( the connectives of S | n) or x in O )

assume x in rng ( the connectives of S | n) ; :: thesis: x in O

then consider y being object such that

A18: ( y in dom ( the connectives of S | n) & x = ( the connectives of S | n) . y ) by FUNCT_1:def 3;

A19: x in the carrier' of S by A18, FUNCT_1:102;

assume x nin O ; :: thesis: contradiction

then x in W by A19, XBOOLE_0:def 5;

then consider z being object such that

A20: ( z in dom ( the connectives of S /^ n) & x = ( the connectives of S /^ n) . z ) by FUNCT_1:def 3;

reconsider y = y as Nat by A18;

reconsider z = z as Nat by A20;

A21: ( y in dom the connectives of S & x = the connectives of S . y ) by A18, RELAT_1:57, FUNCT_1:47;

( y <= len ( the connectives of S | n) & len ( the connectives of S | n) <= n ) by A18, FINSEQ_3:25, FINSEQ_5:17;

then A22: y <= n by XXREAL_0:2;

( ( the connectives of S /^ n) . z = the connectives of S . (z + n) & n + z in dom the connectives of S ) by A10, A20, RFINSEQ:def 1, FINSEQ_5:26;

then ( y = n + z & n = n + 0 ) by A21, A20, FUNCT_1:def 4;

then z = 0 by A22, XREAL_1:6, NAT_1:3;

hence contradiction by A20, FINSEQ_3:24; :: thesis: verum

end;assume x in rng ( the connectives of S | n) ; :: thesis: x in O

then consider y being object such that

A18: ( y in dom ( the connectives of S | n) & x = ( the connectives of S | n) . y ) by FUNCT_1:def 3;

A19: x in the carrier' of S by A18, FUNCT_1:102;

assume x nin O ; :: thesis: contradiction

then x in W by A19, XBOOLE_0:def 5;

then consider z being object such that

A20: ( z in dom ( the connectives of S /^ n) & x = ( the connectives of S /^ n) . z ) by FUNCT_1:def 3;

reconsider y = y as Nat by A18;

reconsider z = z as Nat by A20;

A21: ( y in dom the connectives of S & x = the connectives of S . y ) by A18, RELAT_1:57, FUNCT_1:47;

( y <= len ( the connectives of S | n) & len ( the connectives of S | n) <= n ) by A18, FINSEQ_3:25, FINSEQ_5:17;

then A22: y <= n by XXREAL_0:2;

( ( the connectives of S /^ n) . z = the connectives of S . (z + n) & n + z in dom the connectives of S ) by A10, A20, RFINSEQ:def 1, FINSEQ_5:26;

then ( y = n + z & n = n + 0 ) by A21, A20, FUNCT_1:def 4;

then z = 0 by A22, XREAL_1:6, NAT_1:3;

hence contradiction by A20, FINSEQ_3:24; :: thesis: verum

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: ( len the connectives of S >= 3 & len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) >= 3 & ( for z being Nat st z >= 1 & z <= 3 holds

( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) ) ) )

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;( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) ) ) )

5 <= (m + 1) + 5
by NAT_1:11;

then 3 <= m + 6 by XXREAL_0:2;

hence len the connectives of S >= 3 by A6, XXREAL_0:2; :: thesis: ( len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) >= 3 & ( for z being Nat st z >= 1 & z <= 3 holds

( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) ) ) )

n <= n + (i + 3) by NAT_1:11;

then len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) = n by FINSEQ_1:59, A3, XXREAL_0:2;

hence A23: len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) >= 3 by A12, XXREAL_0:2; :: thesis: for z being Nat st z >= 1 & z <= 3 holds

( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) )

let z be Nat; :: thesis: ( z >= 1 & z <= 3 implies ( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) ) )

assume A24: ( z >= 1 & z <= 3 ) ; :: thesis: ( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) )

then z <= len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) by A23, XXREAL_0:2;

then z in dom the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) by A24, FINSEQ_3:25;

then A25: ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z in O & the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z = the connectives of S . z ) by FUNCT_1:47, FUNCT_1:102;

thus the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) by A25, FUNCT_1:49; :: thesis: the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z)

thus the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) by A25, FUNCT_1:49; :: thesis: verum

end;then 3 <= m + 6 by XXREAL_0:2;

hence len the connectives of S >= 3 by A6, XXREAL_0:2; :: thesis: ( len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) >= 3 & ( for z being Nat st z >= 1 & z <= 3 holds

( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) ) ) )

n <= n + (i + 3) by NAT_1:11;

then len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) = n by FINSEQ_1:59, A3, XXREAL_0:2;

hence A23: len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) >= 3 by A12, XXREAL_0:2; :: thesis: for z being Nat st z >= 1 & z <= 3 holds

( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) )

let z be Nat; :: thesis: ( z >= 1 & z <= 3 implies ( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) ) )

assume A24: ( z >= 1 & z <= 3 ) ; :: thesis: ( the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) )

then z <= len the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) by A23, XXREAL_0:2;

then z in dom the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) by A24, FINSEQ_3:25;

then A25: ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z in O & the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z = the connectives of S . z ) by FUNCT_1:47, FUNCT_1:102;

thus the Arity of S . ( the connectives of S . z) = the Arity of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) by A25, FUNCT_1:49; :: thesis: the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z)

thus the ResultSort of S . ( the connectives of S . z) = the ResultSort of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . ( the connectives of BoolSignature(# the carrier of S,O,A,R, the bool-sort of S,c #) . z) by A25, FUNCT_1:49; :: thesis: verum

reconsider C = ConnectivesSignature(# the carrier of S,W,Ac,Rc,cc #) as non empty non void ConnectivesSignature ;

take B ; :: thesis: ex C being non empty non void ConnectivesSignature st

( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

take C ; :: thesis: ( 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 & B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

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: ( B is n -connectives & B is m,k integer & C is i,j,k -array & 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 )

thus A30: len the connectives of B = n by A9, A3, XXREAL_0:2, FINSEQ_1:59; :: according to AOFA_A00:def 29 :: thesis: ( B is m,k integer & C is i,j,k -array & 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 )

now :: thesis: ( 1 <= m & the bool-sort of B = the bool-sort of S & len the connectives of B >= m + 6 & the connectives of B . m <> the connectives of B . (m + 1) & the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) & ( for z being Nat st z >= m & z <= m + 6 holds

( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) ) )

hence
B is m,k integer
by A8, Th61; :: thesis: ( C is i,j,k -array & 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 )( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) ) )

thus
( 1 <= m & the bool-sort of B = the bool-sort of S )
by A1, XXREAL_0:2; :: thesis: ( len the connectives of B >= m + 6 & the connectives of B . m <> the connectives of B . (m + 1) & the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) & ( for z being Nat st z >= m & z <= m + 6 holds

( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) ) )

thus len the connectives of B >= m + 6 by A2, A9, A3, XXREAL_0:2, FINSEQ_1:59; :: thesis: ( the connectives of B . m <> the connectives of B . (m + 1) & the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) & ( for z being Nat st z >= m & z <= m + 6 holds

( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) ) )

( m <= m + 6 & m + 1 <= (m + 1) + 5 ) by NAT_1:11;

then ( m >= 1 & m <= len the connectives of B & m + 1 >= 1 & m + 1 <= len the connectives of B ) by A1, A2, A30, XXREAL_0:2, NAT_1:11;

then ( m in dom the connectives of B & m + 1 in dom the connectives of B ) by FINSEQ_3:25;

then ( the connectives of B . m = the connectives of S . m & the connectives of B . (m + 1) = the connectives of S . (m + 1) ) by FUNCT_1:47;

hence the connectives of B . m <> the connectives of B . (m + 1) by A7; :: thesis: ( the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) & ( for z being Nat st z >= m & z <= m + 6 holds

( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) ) )

( m + 3 <= (m + 3) + 3 & m + 4 <= (m + 4) + 2 & m + 5 <= (m + 5) + 1 ) by NAT_1:11;

then ( (m + 2) + 1 >= 1 & m + 3 <= len the connectives of B & (m + 3) + 1 >= 1 & m + 4 <= len the connectives of B & (m + 4) + 1 >= 1 & m + 5 <= len the connectives of B ) by A2, A30, XXREAL_0:2, NAT_1:11;

then ( m + 3 in dom the connectives of B & m + 4 in dom the connectives of B & m + 5 in dom the connectives of B ) by FINSEQ_3:25;

then ( the connectives of B . (m + 3) = the connectives of S . (m + 3) & the connectives of B . (m + 4) = the connectives of S . (m + 4) & the connectives of B . (m + 5) = the connectives of S . (m + 5) ) by FUNCT_1:47;

hence ( the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) ) by A7; :: thesis: for z being Nat st z >= m & z <= m + 6 holds

( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) )

let z be Nat; :: thesis: ( z >= m & z <= m + 6 implies ( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) )

assume ( z >= m & z <= m + 6 ) ; :: thesis: ( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) )

then ( 1 <= z & z <= len the connectives of B ) by A2, A30, A13, XXREAL_0:2;

then z in dom the connectives of B by FINSEQ_3:25;

then A31: ( the connectives of B . z in O & the connectives of B . z = the connectives of S . z ) by FUNCT_1:47, FUNCT_1:102;

thus the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) by A31, FUNCT_1:49; :: thesis: the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z)

thus the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) by A31, FUNCT_1:49; :: thesis: verum

end;( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) ) )

thus len the connectives of B >= m + 6 by A2, A9, A3, XXREAL_0:2, FINSEQ_1:59; :: thesis: ( the connectives of B . m <> the connectives of B . (m + 1) & the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) & ( for z being Nat st z >= m & z <= m + 6 holds

( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) ) )

( m <= m + 6 & m + 1 <= (m + 1) + 5 ) by NAT_1:11;

then ( m >= 1 & m <= len the connectives of B & m + 1 >= 1 & m + 1 <= len the connectives of B ) by A1, A2, A30, XXREAL_0:2, NAT_1:11;

then ( m in dom the connectives of B & m + 1 in dom the connectives of B ) by FINSEQ_3:25;

then ( the connectives of B . m = the connectives of S . m & the connectives of B . (m + 1) = the connectives of S . (m + 1) ) by FUNCT_1:47;

hence the connectives of B . m <> the connectives of B . (m + 1) by A7; :: thesis: ( the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) & ( for z being Nat st z >= m & z <= m + 6 holds

( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) ) )

( m + 3 <= (m + 3) + 3 & m + 4 <= (m + 4) + 2 & m + 5 <= (m + 5) + 1 ) by NAT_1:11;

then ( (m + 2) + 1 >= 1 & m + 3 <= len the connectives of B & (m + 3) + 1 >= 1 & m + 4 <= len the connectives of B & (m + 4) + 1 >= 1 & m + 5 <= len the connectives of B ) by A2, A30, XXREAL_0:2, NAT_1:11;

then ( m + 3 in dom the connectives of B & m + 4 in dom the connectives of B & m + 5 in dom the connectives of B ) by FINSEQ_3:25;

then ( the connectives of B . (m + 3) = the connectives of S . (m + 3) & the connectives of B . (m + 4) = the connectives of S . (m + 4) & the connectives of B . (m + 5) = the connectives of S . (m + 5) ) by FUNCT_1:47;

hence ( the connectives of B . (m + 3) <> the connectives of B . (m + 4) & the connectives of B . (m + 3) <> the connectives of B . (m + 5) & the connectives of B . (m + 4) <> the connectives of B . (m + 5) ) by A7; :: thesis: for z being Nat st z >= m & z <= m + 6 holds

( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) )

let z be Nat; :: thesis: ( z >= m & z <= m + 6 implies ( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) ) )

assume ( z >= m & z <= m + 6 ) ; :: thesis: ( the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) & the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) )

then ( 1 <= z & z <= len the connectives of B ) by A2, A30, A13, XXREAL_0:2;

then z in dom the connectives of B by FINSEQ_3:25;

then A31: ( the connectives of B . z in O & the connectives of B . z = the connectives of S . z ) by FUNCT_1:47, FUNCT_1:102;

thus the Arity of S . ( the connectives of S . z) = the Arity of B . ( the connectives of B . z) by A31, FUNCT_1:49; :: thesis: the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z)

thus the ResultSort of S . ( the connectives of S . z) = the ResultSort of B . ( the connectives of B . z) by A31, FUNCT_1:49; :: thesis: verum

now :: thesis: ( len the connectives of C >= i + 3 & 1 <= i & ( for z being Nat st z >= i & z <= i + 3 holds

( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) ) ) )

hence
C is i,j,k -array
by A5, Th62; :: thesis: ( 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 )( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) ) ) )

thus
len the connectives of C >= i + 3
by A11; :: thesis: ( 1 <= i & ( for z being Nat st z >= i & z <= i + 3 holds

( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) ) ) )

thus 1 <= i by A2; :: thesis: for z being Nat st z >= i & z <= i + 3 holds

( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) )

let z be Nat; :: thesis: ( z >= i & z <= i + 3 implies ( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) ) )

assume ( z >= i & z <= i + 3 ) ; :: thesis: ( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) )

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: the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n))

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

end;( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) ) ) )

thus 1 <= i by A2; :: thesis: for z being Nat st z >= i & z <= i + 3 holds

( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) )

let z be Nat; :: thesis: ( z >= i & z <= i + 3 implies ( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) ) )

assume ( z >= i & z <= i + 3 ) ; :: thesis: ( the Arity of C . ( the connectives of C . z) = the Arity of S . ( the connectives of S . (z + n)) & the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n)) )

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: the ResultSort of C . ( the connectives of C . z) = the ResultSort of S . ( the connectives of S . (z + n))

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

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