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);
ex n being Nat st
for i being Nat st i >= n holds
((0_. L) +* (0,x)) . i = 0. L

proof

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

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

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

end;

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

end;

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

now :: thesis: for i being Nat st i < 1 holds
p . i <> 0. L

let i be Nat; :: thesis: ( i < 1 implies p . i <> 0. L )
assume i < 1 ; :: thesis: p . i <> 0. L
then A5: i = 0 by NAT_1:14;
i in NAT by ORDINAL1:def 12;
then 0 in dom (0_. L) by A5, FUNCT_2:def 1;
hence p . i <> 0. L by A2, A5, FUNCT_7:31; :: thesis: verum

end;

then len p <> 0 by ALGSEQ_1:9;
hence p <> 0_. L by POLYNOM4:3; :: according to UPROOTS:def 5 :: thesis: verum