Sum^ (A ^ B) = (Sum^ A) +^ (Sum^ B) by Th24;
hence not Sum^ (A ^ B) is empty ; :: thesis: verum