set p = ((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L);
A1: for i being Nat st i <> 0 & i <> n holds
(((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L

proof

let i be Nat; :: thesis: ( i <> 0 & i <> n implies (((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L )
assume A2: ( i <> 0 & i <> n ) ; :: thesis: (((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L
A3: i in NAT by ORDINAL1:def 13;
set q = (0_. L) +* 0 ,(- (1_ L));
(((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = ((0_. L) +* 0 ,(- (1_ L))) . i by A2, FUNCT_7:34
.= (0_. L) . i by A2, FUNCT_7:34
.= 0. L by A3, FUNCOP_1:13 ;
hence (((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L ; :: thesis: verum

end;

for i being Nat st i >= n + 1 holds
(((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L

proof

let i be Nat; :: thesis: ( i >= n + 1 implies (((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L )
assume A4: i >= n + 1 ; :: thesis: (((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L

now

assume A5: i = n ; :: thesis: contradiction
n + 0 < n + 1 by XREAL_1:10;
hence contradiction by A4, A5; :: thesis: verum

end;

hence (((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L by A1, A4; :: thesis: verum

end;

hence ((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L) is Polynomial of L by ALGSEQ_1:def 2; :: thesis: verum