let L be non empty ZeroStr ; :: thesis: len (0_. L) = 0
for i being Nat st i >= 0 holds
(0_. L) . i = 0. L by FUNCOP_1:7, ORDINAL1:def 12;
then 0 is_at_least_length_of 0_. L ;
hence len (0_. L) = 0 by ALGSEQ_1:def 3; :: thesis: verum