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