now :: thesis: ex x being Element of the carrier of L st x <> 0. L

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

now :: thesis: for x, y being Element of the carrier of L holds y = x

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

end;

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

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

proof

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

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

let i be Nat; :: thesis: ( i >= 2 implies (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L )
assume A3: i >= 2 ; :: thesis: (((0_. L) +* (0,x)) +* (1,x)) . i = 0. L
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: verum

end;

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

end;

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

now :: thesis: for i being Nat st i >= 2 holds
p . i = 0. L

let i be Nat; :: thesis: ( i >= 2 implies p . i = 0. L )
assume A6: i >= 2 ; :: thesis: p . i = 0. L
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: verum

end;

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

now :: thesis: for m being Nat st m is_at_least_length_of p holds
2 <= m

let m be Nat; :: thesis: ( m is_at_least_length_of p implies 2 <= m )
assume A10: m is_at_least_length_of p ; :: thesis: 2 <= m

now :: thesis: not m < 2

assume m < 2 ; :: thesis: contradiction
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: verum

end;

hence 2 <= m ; :: thesis: verum

end;

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