theorem Th63:
for
j,
k being
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 )