now :: thesis: for u being object st u in {0,k} holds
u in NAT
let u be object ; :: 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:62;
A3: k in {k} by TARSKI:def 1;
then A4: k in dom ({k} --> (1_ L)) ;
A5: now :: thesis: for x9 being object st x9 in NAT holds
((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x9 in the carrier of L
let x9 be object ; :: thesis: ( x9 in NAT implies ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . b1 in the carrier of L )
assume x9 in NAT ; :: thesis: ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . b1 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)))) . b1 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:13
.= ((0 .--> (- ((power L) . (z,k)))) +* (k .--> (1_ L))) . x by FUNCT_4:def 4
.= (k .--> (1_ L)) . x by A4, A6, FUNCT_4:13
.= 1_ L by A3, A6, FUNCOP_1:7 ;
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)))) . b1 in the carrier of L
then ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x = - ((power L) . (z,k)) by Lm10;
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)))) . b1 in the carrier of L
then ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x = 1_ L by Lm10;
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)))) . b1 in the carrier of L
then ((0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L)))) . x = 0. L by Lm11;
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)) \/ (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 sequence of the carrier of L by A5, FUNCT_2:3;
reconsider p = p as sequence of L ;
now :: thesis: for i being Nat st i >= k + 1 holds
p . i = 0. L
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, Lm11; :: thesis: verum
end;
then reconsider p = p as AlgSequence of L by ALGSEQ_1:def 1;
p is Polynomial of L ;
hence (0_. L) +* ((0,k) --> ((- ((power L) . (z,k))),(1_ L))) is Polynomial of L ; :: thesis: verum