assume A1: for x being Element of the carrier of L holds not x <> 0. L ; :: thesis:

let x, y be Element of the carrier of L; :: thesis:
thus y = 0. L by A1
.= x by A1 ; :: thesis:

end;

hence contradiction by STRUCT_0:def 10; :: thesis:

end;

then consider x being Element of the carrier of L such that
A2: x <> 0. L ;
set p = ((0_. L) +* (0,x)) +* (1,x);
ex n being Nat st
for i being Nat st i >= n holds
(((0_. L) +* (0,x)) +* (1,x)) . i = 0. L

take 2 ; :: thesis:

let i be Nat; :: thesis:
assume A3: i >= 2 ; :: thesis:
then A4: 1 <> i ;
A5: i in NAT by ORDINAL1:def 12;
thus (((0_. L) +* (0,x)) +* (1,x)) . i = ((0_. L) +* (0,x)) . i by A4, FUNCT_7:32
.= (0_. L) . i by A3, FUNCT_7:32
.= 0. L by A5, FUNCOP_1:7 ; :: thesis:

end;

hence for i being Nat st i >= 2 holds
(((0_. L) +* (0,x)) +* (1,x)) . i = 0. L ; :: thesis:

end;

then reconsider p = ((0_. L) +* (0,x)) +* (1,x) as Polynomial of L by ALGSEQ_1:def 1;
take p ; :: thesis:

let i be Nat; :: thesis:
assume A6: i >= 2 ; :: thesis:
then A7: 1 <> i ;
A8: i in NAT by ORDINAL1:def 12;
thus p . i = ((0_. L) +* (0,x)) . i by A7, FUNCT_7:32
.= (0_. L) . i by A6, FUNCT_7:32
.= 0. L by A8, FUNCOP_1:7 ; :: thesis:

end;

then A9: 2 is_at_least_length_of p by ALGSEQ_1:def 2;

let m be Nat; :: thesis:
assume A10: m is_at_least_length_of p ; :: thesis:

assume m < 2 ; :: thesis:
then m < 1 + 1 ;
then m <= 1 by NAT_1:13;
then A11: p . 1 = 0. L by A10, ALGSEQ_1:def 2;
dom (0_. L) = NAT by FUNCOP_1:13;
then dom ((0_. L) +* (0,x)) = NAT by FUNCT_7:30;
hence contradiction by A2, A11, FUNCT_7:31; :: thesis:

end;

hence 2 <= m ; :: thesis:

end;

then len p = 2 by A9, ALGSEQ_1:def 3;
then deg p = 1 ;
hence not p is constant ; :: thesis: