let L be non empty non degenerated multLoopStr_0 ; :: thesis: len (1_. L) = 1

A1: now :: thesis: for i being Nat st i is_at_least_length_of 1_. L holds
not 0 + 1 > i

let i be Nat; :: thesis: ( i is_at_least_length_of 1_. L implies not 0 + 1 > i )
assume that
A2: i is_at_least_length_of 1_. L and
A3: 0 + 1 > i ; :: thesis: contradiction
0 >= i by A3, NAT_1:13;
then (1_. L) . 0 = 0. L by A2;
hence contradiction by POLYNOM3:30; :: thesis: verum

end;

for i being Nat st i >= 1 holds
(1_. L) . i = 0. L by POLYNOM3:30;
then 1 is_at_least_length_of 1_. L ;
hence len (1_. L) = 1 by A1, ALGSEQ_1:def 3; :: thesis: verum