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

set q = (0_. L) +* (0,(- (1_ L)));
let i be Nat; :: thesis: ( i <> 0 & i <> n implies (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L )
assume that
A2: i <> 0 and
A3: i <> n ; :: thesis: (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L
A4: i in NAT by ORDINAL1:def 12;
(((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = ((0_. L) +* (0,(- (1_ L)))) . i by A3, FUNCT_7:32
.= (0_. L) . i by A2, FUNCT_7:32
.= 0. L by A4, FUNCOP_1:7 ;
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 A5: i >= n + 1 ; :: thesis: (((0_. L) +* (0,(- (1_ L)))) +* (n,(1_ L))) . i = 0. L

now :: thesis: not i = n

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

end;

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

end;

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