let A be Ordinal-Sequence; :: thesis: ( A is Cantor-normal-form implies A is non-empty )
assume A1: A is Cantor-normal-form ; :: thesis: A is non-empty

now :: thesis: for x being object st x in dom A holds
not A . x is empty

let x be object ; :: thesis: ( x in dom A implies not A . x is empty )
assume x in dom A ; :: thesis: not A . x is empty
then A . x is Cantor-component by A1;
hence not A . x is empty ; :: thesis: verum

end;

hence A is non-empty by FUNCT_1:def 9; :: thesis: verum