now

let u be set ; :: thesis: ( u in {0 ,k} implies u in NAT )
assume u in {0 ,k} ; :: thesis: u in NAT
then ( u = 0 or u = k ) by TARSKI:def 2;
hence u in NAT ; :: thesis: verum

end;

then A1: {0 ,k} c= NAT by TARSKI:def 3;
set a = - ((power L) . z,k);
set p = (0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L));
set f = 0 ,k --> (- ((power L) . z,k)),(1_ L);
A2: dom (0 ,k --> (- ((power L) . z,k)),(1_ L)) = {0 ,k} by FUNCT_4:65;
A3: k in {k} by TARSKI:def 1;
then A4: k in dom ({k} --> (1_ L)) by FUNCOP_1:19;

A5: now

let x9 be set ; :: thesis: ( x9 in NAT implies ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . b₁ in the carrier of L )
assume x9 in NAT ; :: thesis: ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . b₁ in the carrier of L
then reconsider x = x9 as Element of NAT ;

per cases ( ( k = 0 & x = 0 ) or ( x = 0 & k <> 0 ) or ( x = k & k <> 0 ) or ( x <> 0 & x <> k ) ) ;

suppose A6: ( k = 0 & x = 0 ) ; :: thesis: ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . b₁ in the carrier of L

then x in dom (0 ,k --> (- ((power L) . z,k)),(1_ L)) by A2, TARSKI:def 2;
then ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x = (0 ,k --> (- ((power L) . z,k)),(1_ L)) . x by FUNCT_4:14
.= ((0 .--> (- ((power L) . z,k))) +* (k .--> (1_ L))) . x by FUNCT_4:def 4
.= (k .--> (1_ L)) . x by A4, A6, FUNCT_4:14
.= 1_ L by A3, A6, FUNCOP_1:13 ;
hence ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x9 in the carrier of L ; :: thesis: verum

end;

suppose ( x = 0 & k <> 0 ) ; :: thesis: ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . b₁ in the carrier of L

then ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x = - ((power L) . z,k) by Lm11;
hence ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x9 in the carrier of L ; :: thesis: verum

end;

suppose ( x = k & k <> 0 ) ; :: thesis: ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . b₁ in the carrier of L

then ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x = 1_ L by Lm11;
hence ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x9 in the carrier of L ; :: thesis: verum

end;

suppose ( x <> 0 & x <> k ) ; :: thesis: ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . b₁ in the carrier of L

then ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x = 0. L by Lm12;
hence ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x9 in the carrier of L ; :: thesis: verum

end;

end;

end;

dom (0_. L) = NAT by FUNCT_2:def 1;
then (dom (0_. L)) \/ (dom (0 ,k --> (- ((power L) . z,k)),(1_ L))) = NAT by A2, A1, XBOOLE_1:12;
then dom ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) = NAT by FUNCT_4:def 1;
then reconsider p = (0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L)) as Function of NAT ,the carrier of L by A5, FUNCT_2:5;
reconsider p = p as sequence of L ;

now

let i be Nat; :: thesis: ( i >= k + 1 implies p . i = 0. L )
assume A7: i >= k + 1 ; :: thesis: p . i = 0. L
then i <> k by NAT_1:13;
hence p . i = 0. L by A7, Lm12; :: thesis: verum

end;

then reconsider p = p as AlgSequence of L by ALGSEQ_1:def 2;
p is Polynomial of L ;
hence (0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L)) is Polynomial of L ; :: thesis: verum