the carrier of (B +* C) = the carrier of B \/ the carrier of C
by CIRCCOMB:def 2;
then reconsider b = the bool-sort of B as SortSymbol of (B +* C) by XBOOLE_0:def 3;
A1:
the carrier' of (B +* C) = the carrier' of B \/ the carrier' of C
by CIRCCOMB:def 2;
( rng the connectives of B c= the carrier' of B & rng the connectives of C c= the carrier' of C )
by RELAT_1:def 19;
then
(rng the connectives of B) \/ (rng the connectives of C) c= the carrier' of (B +* C)
by A1, XBOOLE_1:13;
then
rng ( the connectives of B ^ the connectives of C) c= the carrier' of (B +* C)
by FINSEQ_1:31;
then reconsider c = the connectives of B ^ the connectives of C as FinSequence of the carrier' of (B +* C) by FINSEQ_1:def 4;
take
BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #)
; ( ManySortedSign(# the carrier of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #), the carrier' of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #), the Arity of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #), the ResultSort of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #) #) = B +* C & the bool-sort of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #) = the bool-sort of B & the connectives of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #) = the connectives of B ^ the connectives of C )
thus
( ManySortedSign(# the carrier of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #), the carrier' of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #), the Arity of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #), the ResultSort of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #) #) = B +* C & the bool-sort of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #) = the bool-sort of B & the connectives of BoolSignature(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C),b,c #) = the connectives of B ^ the connectives of C )
; verum