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 13;
(((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = ((0_. L) +* 0 ,(- (1_ L))) . i by A3, FUNCT_7:34
.= (0_. L) . i by A2, FUNCT_7:34
.= 0. L by A4, 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 A5: i >= n + 1 ; :: thesis: (((0_. L) +* 0 ,(- (1_ L))) +* n,(1_ L)) . i = 0. L

now

A6: n + 0 < n + 1 by XREAL_1:10;
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 2; :: thesis: verum