let A be Cantor-normal-form Ordinal-Sequence; :: thesis: ( Sum^ A = 0 implies A = {} )
assume A0: ( Sum^ A = 0 & A <> {} ) ; :: thesis: contradiction
then 0 in dom A by ORDINAL3:10;
then reconsider a = A . 0 as Cantor-component Ordinal by CNF;
( 0 in a & a c= Sum^ A ) by Th53, ORDINAL3:10;
hence contradiction by A0; :: thesis: verum