0 c< dom A by XBOOLE_1:2, XBOOLE_0:def 8;
then A1: 0 in dom A by ORDINAL1:11;
A . 0 c= Sum^ A by ORDINAL5:56;
hence not Sum^ A is empty by A1; :: thesis: verum