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
.= (0_. L) . i by
.= 0. L by ;
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