let L be non empty ZeroStr ; :: thesis: len (0_. L) = 0

now

let i be Nat; :: thesis: ( i >= 0 implies (0_. L) . i = 0. L )
i in NAT by ORDINAL1:def 13;
hence ( i >= 0 implies (0_. L) . i = 0. L ) by FUNCOP_1:13; :: thesis: verum

end;

then 0 is_at_least_length_of 0_. L by ALGSEQ_1:def 3;
hence len (0_. L) = 0 by ALGSEQ_1:def 4; :: thesis: verum