let j, k be set ; 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; ( 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
; ( 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 )
; 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 ; ( 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
; AOFA_A00:def 50 ( 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 )
; ( 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
; AOFA_A00:def 38 ( 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 )
; 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;
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
let x be
object ;
TARSKI:def 3 ( not x in rng ( the connectives of S | n) or x in O )
assume
x in rng ( the connectives of S | n)
;
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
;
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;
verum
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 ( 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) ) ) )
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;
( 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;
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;
( 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 )
;
( 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;
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;
verum 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
; 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
; ( 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; ( 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; AOFA_A00:def 29 ( 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 ( 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) ) ) )thus
( 1
<= m & the
bool-sort of
B = the
bool-sort of
S )
by A1, XXREAL_0:2;
( 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;
( 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;
( 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;
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;
( 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 )
;
( 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;
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;
verum end;
hence
B is m,k integer
by A8, Th61; ( 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 )
hence
C is i,j,k -array
by A5, Th62; ( 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 )
; verum