let S1, S2 be non empty ManySortedSign ; :: thesis: ( ( not S1 is void or not S2 is void ) implies not S1 +* S2 is void )
consider o1 being Gate of S1, o2 being Gate of S2;
Lm2: for S being non void ManySortedSign
for o being Gate of S holds o in the carrier' of S ;
assume ( not S1 is void or not S2 is void ) ; :: thesis: not S1 +* S2 is void
then ( ( o1 in the carrier' of S1 or o2 in the carrier' of S2 ) & the carrier' of (S1 +* S2) = the carrier' of S1 \/ the carrier' of S2 ) by Def2, Lm2;
hence not the carrier' of (S1 +* S2) is empty ; :: according to STRUCT_0:def 13 :: thesis: verum