let p be prime odd Nat; :: thesis: for m being positive Nat
for k, j being Nat st j in Seg m & p <= k holds
ex u, v being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = ((tau j) * u) + ((p !) * v)
let m be positive Nat; :: thesis: for k, j being Nat st j in Seg m & p <= k holds
ex u, v being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = ((tau j) * u) + ((p !) * v)
let k, j be Nat; :: thesis: ( j in Seg m & p <= k implies ex u, v being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = ((tau j) * u) + ((p !) * v) )
set D = Der1 INT.Ring;
set PR = Polynom-Ring INT.Ring;
set tj = tau j;
set gj = Product (Del ((ff_0 (m,p)),j));
assume A1: ( j in Seg m & p <= k ) ; :: thesis: ex u, v being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = ((tau j) * u) + ((p !) * v)
set p1 = p + 1;
A2: ( 1 <= p & p <= k ) by A1, INT_2:def 4;
1. (Polynom-Ring INT.Ring) = (Der1 INT.Ring) . (tau j) by Th27
.= ((Der1 INT.Ring) |^ 1) . (tau j) by VECTSP11:19
.= ((Der1 INT.Ring) |^ 1) . ((tau j) |^ 1) by BINOM:8 ;
then A3: ((Der1 INT.Ring) |^ ((p + 1) -' 1)) . ((tau j) |^ p) = (eta (p,p)) * ((tau j) |^ (p -' p)) by A2, E_TRANS1:19
.= (eta (p,p)) * ((tau j) |^ 0) by XREAL_1:232
.= (eta (p,p)) * (1_ (Polynom-Ring INT.Ring)) by BINOM:8
.= (p !) * (1. (Polynom-Ring INT.Ring)) by Lm5 ;
A4: len (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) = k + 1 by RINGDER1:def 4;
then A5: dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) = Seg (k + 1) by FINSEQ_1:def 3;
A6: 0 + 1 <= p + 1 by XREAL_1:6;
A7: (k + 1) -' (p + 1) = (k + 1) - (p + 1) by A1, XREAL_1:6, XREAL_1:233
.= k - p
.= k -' p by A1, XREAL_1:233 ;
( 1 <= p + 1 & p + 1 <= k + 1 ) by A1, XREAL_1:6, A6;
then A9: p + 1 in dom (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) by A5;
reconsider lbz = LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p)) as non empty FinSequence of the carrier of (Polynom-Ring INT.Ring) by A4;
reconsider p9 = p ! as Element of NAT by ORDINAL1:def 12;
A10: (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) . (p + 1) = ((k choose p) * (((Der1 INT.Ring) |^ (k -' p)) . (Product (Del ((ff_0 (m,p)),j))))) * (p9 * (1. (Polynom-Ring INT.Ring))) by A7, A3, A9, RINGDER1:def 4
.= (((k choose p) * (((Der1 INT.Ring) |^ (k -' p)) . (Product (Del ((ff_0 (m,p)),j))))) * (1. (Polynom-Ring INT.Ring))) * p9 by BINOM:20
.= p9 * ((k choose p) * (((Der1 INT.Ring) |^ (k -' p)) . (Product (Del ((ff_0 (m,p)),j))))) by BINOM:18 ;
p <= len lbz by A1, A4, XREAL_1:39;
then A12: len (lbz | p) = p by FINSEQ_1:59;
then A13: dom (lbz | p) = Seg p by FINSEQ_1:def 3;
set lbz1 = lbz | p;
A14: p <= k + 1 by A1, XREAL_1:39;
for i being Nat st i in Seg p holds
tau j divides (lbz | p) /. i

proof

let i be Nat; :: thesis: ( i in Seg p implies tau j divides (lbz | p) /. i )
assume A16: i in Seg p ; :: thesis: tau j divides (lbz | p) /. i
then ( 1 <= i & i <= p ) by FINSEQ_1:1;
then ( 1 <= i & i <= k + 1 ) by A14, XXREAL_0:2;
then A18: i in dom lbz by A5;
i in dom (lbz | p) by A12, FINSEQ_1:def 3, A16;
then (lbz | p) /. i = (lbz | p) . i by PARTFUN1:def 6
.= lbz . i by A16, FUNCT_1:49
.= lbz /. i by A18, PARTFUN1:def 6 ;
hence tau j divides (lbz | p) /. i by A1, A16, Th28; :: thesis: verum

end;

then consider u being Element of (Polynom-Ring INT.Ring) such that
A20: Sum (lbz | p) = (tau j) * u by GCD_1:def 1, A13, E_TRANS1:4;
A21: len (lbz /^ (p + 1)) = (len lbz) -' (p + 1) by RFINSEQ:29
.= (k + 1) -' (p + 1) by RINGDER1:def 4 ;
A22: dom (lbz /^ (p + 1)) = Seg ((k + 1) -' (p + 1)) by A21, FINSEQ_1:def 3;
set kp1 = (k + 1) -' (p + 1);
A23: for i1 being Nat st i1 in dom (lbz /^ (p + 1)) holds
(lbz /^ (p + 1)) /. i1 = 0. (Polynom-Ring INT.Ring)

proof

let i1 be Nat; :: thesis: ( i1 in dom (lbz /^ (p + 1)) implies (lbz /^ (p + 1)) /. i1 = 0. (Polynom-Ring INT.Ring) )
assume A24: i1 in dom (lbz /^ (p + 1)) ; :: thesis: (lbz /^ (p + 1)) /. i1 = 0. (Polynom-Ring INT.Ring)
then A25: ( 1 <= i1 & i1 <= (k + 1) -' (p + 1) ) by A22, FINSEQ_1:1;
set pi1 = (p + 1) + i1;
(k + 1) -' (p + 1) = (k + 1) - (p + 1) by A1, XREAL_1:6, XREAL_1:233;
then (p + 1) + i1 <= ((k + 1) - (p + 1)) + (p + 1) by A25, XREAL_1:6;
then ( 1 <= (p + 1) + i1 & (p + 1) + i1 <= k + 1 ) by A25, XREAL_1:39;
then A29: (p + 1) + i1 in dom lbz by A5;
A30: p + 1 < (p + 1) + i1 by A25, XREAL_1:39;
(lbz /^ (p + 1)) /. i1 = lbz /. ((p + 1) + i1) by A24, FINSEQ_5:27;
hence (lbz /^ (p + 1)) /. i1 = 0. (Polynom-Ring INT.Ring) by A30, A29, Th29; :: thesis: verum

end;

lbz /^ (p + 1) = ((k + 1) -' (p + 1)) |-> (0. (Polynom-Ring INT.Ring))

proof

for k being Nat st k in dom (lbz /^ (p + 1)) holds
(lbz /^ (p + 1)) . k = (((k + 1) -' (p + 1)) |-> (0. (Polynom-Ring INT.Ring))) . k

proof

let k be Nat; :: thesis: ( k in dom (lbz /^ (p + 1)) implies (lbz /^ (p + 1)) . k = (((k + 1) -' (p + 1)) |-> (0. (Polynom-Ring INT.Ring))) . k )
assume A31: k in dom (lbz /^ (p + 1)) ; :: thesis: (lbz /^ (p + 1)) . k = (((k + 1) -' (p + 1)) |-> (0. (Polynom-Ring INT.Ring))) . k
then A32: k in Seg ((k + 1) -' (p + 1)) by A21, FINSEQ_1:def 3;
(lbz /^ (p + 1)) . k = (lbz /^ (p + 1)) /. k by A31, PARTFUN1:def 6
.= 0. (Polynom-Ring INT.Ring) by A31, A23 ;
hence (lbz /^ (p + 1)) . k = (((k + 1) -' (p + 1)) |-> (0. (Polynom-Ring INT.Ring))) . k by A32, FINSEQ_2:57; :: thesis: verum

end;

hence lbz /^ (p + 1) = ((k + 1) -' (p + 1)) |-> (0. (Polynom-Ring INT.Ring)) by A21, FINSEQ_1:def 3; :: thesis: verum

end;

then Sum (lbz /^ (p + 1)) = 0. (Polynom-Ring INT.Ring) by MATRIX_3:11;
then A34: Sum (<*(lbz /. (p + 1))*> ^ (lbz /^ (p + 1))) = (lbz /. (p + 1)) + (0. (Polynom-Ring INT.Ring)) by FVSUM_1:72
.= lbz /. (p + 1) ;
( 1 <= p + 1 & p + 1 <= len lbz ) by A1, XREAL_1:6, A6, A4;
then lbz = ((lbz | ((p + 1) -' 1)) ^ <*(lbz . (p + 1))*>) ^ (lbz /^ (p + 1)) by FINSEQ_5:84
.= ((lbz | p) ^ <*(lbz /. (p + 1))*>) ^ (lbz /^ (p + 1)) by A9, PARTFUN1:def 6
.= (lbz | p) ^ (<*(lbz /. (p + 1))*> ^ (lbz /^ (p + 1))) by FINSEQ_1:32 ;
then A36: Sum lbz = ((tau j) * u) + (lbz /. (p + 1)) by A34, A20, RLVECT_1:41
.= ((tau j) * u) + ((p !) * ((k choose p) * (((Der1 INT.Ring) |^ (k -' p)) . (Product (Del ((ff_0 (m,p)),j)))))) by A10, A9, PARTFUN1:def 6 ;
Sum lbz = ((Der1 INT.Ring) |^ k) . ((Product (Del ((ff_0 (m,p)),j))) * ((tau j) |^ p)) by RINGDER1:25
.= ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) by A1, Lm9 ;
hence ex u, v being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = ((tau j) * u) + ((p !) * v) by A36; :: thesis: verum