per cases ( a = 0. L or a <> 0. L ) ;

suppose a = 0. L ; :: thesis: a | L is constant

then a | L = 0_. L by T6;
then len (a | L) = 0 by POLYNOM4:3;
then deg (a | L) = - 1 ;
hence a | L is constant by RATFUNC1:def 2; :: thesis: verum

end;

suppose A0: a <> 0. L ; :: thesis: a | L is constant

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

let i be Nat; :: thesis: ( i is_at_least_length_of a | L implies not 0 + 1 > i )
assume that
A2: i is_at_least_length_of a | L and
A3: 0 + 1 > i ; :: thesis: contradiction
0 >= i by A3, NAT_1:13;
then (a | L) . 0 = 0. L by A2, ALGSEQ_1:def 2;
hence contradiction by A0, Th28; :: thesis: verum

end;

for i being Nat st i >= 1 holds
(a | L) . i = 0. L by Th28;
then len (a | L) = 1 by A1, ALGSEQ_1:def 3, ALGSEQ_1:def 2;
then deg (a | L) = 0 ;
hence a | L is constant by RATFUNC1:def 2; :: thesis: verum

end;

end;