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;