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