let B be non empty BoolSignature ; :: thesis: for C being non empty ConnectivesSignature holds
( the carrier of (B +* C) = the carrier of B \/ the carrier of C & the carrier' of (B +* C) = the carrier' of B \/ the carrier' of C & 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 )
let C be non empty ConnectivesSignature ; :: thesis: ( the carrier of (B +* C) = the carrier of B \/ the carrier of C & the carrier' of (B +* C) = the carrier' of B \/ the carrier' of C & 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 )
ManySortedSign(# the carrier of (B +* C), the carrier' of (B +* C), the Arity of (B +* C), the ResultSort of (B +* C) #) = B +* C by Def52;
hence ( the carrier of (B +* C) = the carrier of B \/ the carrier of C & the carrier' of (B +* C) = the carrier' of B \/ the carrier' of C & 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 CIRCCOMB:def 2; :: thesis: verum