let B be non empty non void bool-correct BoolSignature ; for C being non empty non void ConnectivesSignature st the carrier' of B misses the carrier' of C holds
B +* C is bool-correct
let C be non empty non void ConnectivesSignature ; ( the carrier' of B misses the carrier' of C implies B +* C is bool-correct )
assume A1:
the carrier' of B misses the carrier' of C
; B +* C is bool-correct
set S = B +* C;
A2:
the connectives of (B +* C) = the connectives of B ^ the connectives of C
by Def52;
then A3:
len the connectives of (B +* C) = (len the connectives of B) + (len the connectives of C)
by FINSEQ_1:22;
A4:
len the connectives of B >= 3
by Def30;
hence
len the connectives of (B +* C) >= 3
by A3, NAT_1:12; AOFA_A00:def 30 ( the connectives of (B +* C) . 1 is_of_type {} , the bool-sort of (B +* C) & the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C) & the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C) )
A5:
now for i being Nat st 1 <= i & i <= len the connectives of B holds
( the connectives of (B +* C) . i = the connectives of B . i & ( for x being set
for I being Element of B
for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds
the connectives of (B +* C) . i is_of_type x,J ) )let i be
Nat;
( 1 <= i & i <= len the connectives of B implies ( the connectives of (B +* C) . i = the connectives of B . i & ( for x being set
for I being Element of B
for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds
the connectives of (B +* C) . i is_of_type x,J ) ) )assume
( 1
<= i &
i <= len the
connectives of
B )
;
( the connectives of (B +* C) . i = the connectives of B . i & ( for x being set
for I being Element of B
for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds
the connectives of (B +* C) . i is_of_type x,J ) )then A6:
i in dom the
connectives of
B
by FINSEQ_3:25;
then
the
connectives of
B . i in the
carrier' of
B
by FUNCT_1:102;
then A7:
the
connectives of
B . i nin the
carrier' of
C
by A1, XBOOLE_0:3;
A8:
(
dom the
Arity of
C = the
carrier' of
C &
dom the
ResultSort of
C = the
carrier' of
C )
by FUNCT_2:def 1;
( the
Arity of
(B +* C) = the
Arity of
B +* the
Arity of
C & the
ResultSort of
(B +* C) = the
ResultSort of
B +* the
ResultSort of
C )
by Th51;
then A9:
( the
Arity of
(B +* C) . ( the connectives of B . i) = the
Arity of
B . ( the connectives of B . i) & the
ResultSort of
(B +* C) . ( the connectives of B . i) = the
ResultSort of
B . ( the connectives of B . i) )
by A7, A8, FUNCT_4:11;
thus A10:
the
connectives of
(B +* C) . i = the
connectives of
B . i
by A2, A6, FINSEQ_1:def 7;
for x being set
for I being Element of B
for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds
the connectives of (B +* C) . i is_of_type x,Jlet x be
set ;
for I being Element of B
for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds
the connectives of (B +* C) . i is_of_type x,Jlet I be
Element of
B;
for J being Element of (B +* C) st I = J & the connectives of B . i is_of_type x,I holds
the connectives of (B +* C) . i is_of_type x,Jlet J be
Element of
(B +* C);
( I = J & the connectives of B . i is_of_type x,I implies the connectives of (B +* C) . i is_of_type x,J )assume A11:
(
I = J & the
connectives of
B . i is_of_type x,
I )
;
the connectives of (B +* C) . i is_of_type x,Jthus
the
connectives of
(B +* C) . i is_of_type x,
J
by A9, A11, A10;
verum end;
A12:
the bool-sort of (B +* C) = the bool-sort of B
by Def52;
A13:
1 <= len the connectives of B
by A4, XXREAL_0:2;
the connectives of B . 1 is_of_type {} , the bool-sort of B
by Def30;
hence
the connectives of (B +* C) . 1 is_of_type {} , the bool-sort of (B +* C)
by A5, A12, A13; ( the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C) & the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C) )
A14:
2 <= len the connectives of B
by A4, XXREAL_0:2;
the connectives of B . 2 is_of_type <* the bool-sort of B*>, the bool-sort of B
by Def30;
hence
the connectives of (B +* C) . 2 is_of_type <* the bool-sort of (B +* C)*>, the bool-sort of (B +* C)
by A5, A12, A14; the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C)
the connectives of B . 3 is_of_type <* the bool-sort of B, the bool-sort of B*>, the bool-sort of B
by Def30;
hence
the connectives of (B +* C) . 3 is_of_type <* the bool-sort of (B +* C), the bool-sort of (B +* C)*>, the bool-sort of (B +* C)
by A5, A4, A12; verum