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 #) ; :: thesis: ( 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 ) ; :: thesis: verum

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 #) ; :: thesis: ( 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 ) ; :: thesis: verum