let S1, S2 be non empty ManySortedSign ; :: thesis: ( ( not S1 is void or not S2 is void ) implies not S1 +* S2 is void )
assume A1: ( not S1 is void or not S2 is void ) ; :: thesis: not S1 +* S2 is void
the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 by Def2;
hence not the carrier' of (S1 +* S2) is empty by A1; :: according to STRUCT_0:def 13 :: thesis: verum