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

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 {0 ,k} c= NAT by TARSKI:def 3;
then (dom (0_. L)) \/ (dom (0 ,k --> (- ((power L) . z,k)),(1_ L))) = NAT by A3, A4, XBOOLE_1:12;
then A5: dom ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) = NAT by FUNCT_4:def 1;

now

let x' be set ; :: thesis: ( x' in NAT implies ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . b₁ in the carrier of L )
assume x' in NAT ; :: thesis: ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . b₁ in the carrier of L
then reconsider x = x' 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 A3, 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 A2, A6, FUNCT_4:14
.= 1_ L by A1, A6, FUNCOP_1:13 ;
hence ((0_. L) +* (0 ,k --> (- ((power L) . z,k)),(1_ L))) . x' 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))) . x' 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))) . x' 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))) . x' in the carrier of L ; :: thesis: verum

end;

end;

end;

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 i >= k + 1 ; :: thesis: p . i = 0. L
then ( i <> 0 & i <> k ) by NAT_1:13;
hence p . i = 0. L by 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