set S = the non empty non void ManySortedSign ;
set o = the OperSymbol of the non empty non void ManySortedSign ;
reconsider c = n |-> the OperSymbol of the non empty non void ManySortedSign as n -element FinSequence of the carrier' of the non empty non void ManySortedSign ;
take C = ConnectivesSignature(# the carrier of the non empty non void ManySortedSign , the carrier' of the non empty non void ManySortedSign , the Arity of the non empty non void ManySortedSign , the ResultSort of the non empty non void ManySortedSign ,c #); :: thesis: ( C is n -connectives & not C is empty & not C is void )
thus len the connectives of C = n by CARD_1:def 7; :: according to AOFA_A00:def 29 :: thesis: ( not C is empty & not C is void )
thus not the carrier of C is empty ; :: according to STRUCT_0:def 1 :: thesis: not C is void
thus not the carrier' of C is empty ; :: according to STRUCT_0:def 13 :: thesis: verum