set DR = Der1 INT.Ring;
set PRF = Polynom-Ring F_Real;
set PRI = Polynom-Ring INT.Ring;
let f be Element of the carrier of (Polynom-Ring INT.Ring); ( len f > 0 implies ( (Sum ('G' f)) - f = (Der1 INT.Ring) . (Sum ('G' f)) & (Sum ('G' f)) - f = (Der1 INT.Ring) . (Sum ('G' f)) & Sum ('G' f) = ((Der1 INT.Ring) . (Sum ('G' f))) + f ) )
assume A1:
len f > 0
; ( (Sum ('G' f)) - f = (Der1 INT.Ring) . (Sum ('G' f)) & (Sum ('G' f)) - f = (Der1 INT.Ring) . (Sum ('G' f)) & Sum ('G' f) = ((Der1 INT.Ring) . (Sum ('G' f))) + f )
A2:
1 <= len f
by A1, NAT_1:14;
reconsider l1 = (len f) -' 1 as Nat ;
A3:
l1 = (len f) - 1
by A1, NAT_1:14, XREAL_1:233;
A4:
len ('G' f) = len f
by Def9;
then
dom ('G' f) = Seg (len f)
by FINSEQ_1:def 3;
then A8:
1 in dom ('G' f)
by A2;
rng ('G' f) c= the carrier of (Polynom-Ring INT.Ring)
;
then
rng ('G' f) c= dom (Der1 INT.Ring)
by FUNCT_2:def 1;
then A6: len ((Der1 INT.Ring) * ('G' f)) =
len ('G' f)
by FINSEQ_2:29
.=
len f
by Def9
;
then A7:
dom ((Der1 INT.Ring) * ('G' f)) = Seg (len f)
by FINSEQ_1:def 3;
reconsider Gf = 'G' f as non empty FinSequence of the carrier of (Polynom-Ring INT.Ring) by A1, A4;
A9: ('G' f) . 1 =
((Der1 INT.Ring) |^ (1 -' 1)) . f
by A8, Def9
.=
((Der1 INT.Ring) |^ 0) . f
by XREAL_1:232
.=
(id (Polynom-Ring INT.Ring)) . f
by VECTSP11:18
.=
f
;
Gf = <*(Gf . 1)*> ^ (Del (Gf,1))
by FINSEQ_5:86;
then A10: Sum Gf =
Sum (<*(Gf /. 1)*> ^ (Del (Gf,1)))
by A8, PARTFUN1:def 6
.=
(Sum <*(Gf /. 1)*>) + (Sum (Del (Gf,1)))
by RLVECT_1:41
.=
(Gf /. 1) + (Sum (Del (Gf,1)))
by RLVECT_1:44
.=
f + (Sum (Del (Gf,1)))
by A9, A8, PARTFUN1:def 6
;
A12:
l1 + 1 in dom ((Der1 INT.Ring) * ('G' f))
by A7, A3, FINSEQ_1:3;
l1 + 1 in Seg (len f)
by A3, FINSEQ_1:3;
then A13:
len f in dom ('G' f)
by A4, FINSEQ_1:def 3, A3;
reconsider Gff = ('G' f) . (len f) as constant Element of the carrier of (Polynom-Ring INT.Ring) by Lm17, A1;
A14: ((Der1 INT.Ring) * ('G' f)) /. (len f) =
((Der1 INT.Ring) * ('G' f)) . (len f)
by A3, A12, PARTFUN1:def 6
.=
(Der1 INT.Ring) . Gff
by A13, FUNCT_1:13
.=
0_. INT.Ring
by FIELD_14:60
.=
0. (Polynom-Ring INT.Ring)
by POLYNOM3:def 10
;
(Der1 INT.Ring) * ('G' f) =
((Der1 INT.Ring) * ('G' f)) | (l1 + 1)
by A3, A6
.=
(((Der1 INT.Ring) * ('G' f)) | l1) ^ <*(((Der1 INT.Ring) * ('G' f)) . (l1 + 1))*>
by A6, A3, XREAL_1:44, FINSEQ_5:83
;
then Sum ((Der1 INT.Ring) * ('G' f)) =
Sum ((((Der1 INT.Ring) * ('G' f)) | l1) ^ <*(((Der1 INT.Ring) * ('G' f)) /. (l1 + 1))*>)
by PARTFUN1:def 6, A3, A7, FINSEQ_1:3
.=
(Sum (((Der1 INT.Ring) * ('G' f)) | l1)) + (Sum <*(((Der1 INT.Ring) * ('G' f)) /. (len f))*>)
by A3, RLVECT_1:41
.=
(Sum (((Der1 INT.Ring) * ('G' f)) | l1)) + (0. (Polynom-Ring INT.Ring))
by A14, RLVECT_1:44
.=
Sum (((Der1 INT.Ring) * ('G' f)) | l1)
;
then A17:
(Der1 INT.Ring) . (Sum ('G' f)) = Sum (((Der1 INT.Ring) * ('G' f)) | l1)
by Th23;
A18: (Sum Gf) - f =
(Sum (Del (Gf,1))) + (f + (- f))
by RLVECT_1:def 3, A10
.=
(Sum (Del (Gf,1))) + (0. (Polynom-Ring INT.Ring))
by RLVECT_1:def 10
.=
(Der1 INT.Ring) . (Sum ('G' f))
by A17, Lm18, A1
;
((Der1 INT.Ring) . (Sum ('G' f))) + f =
(Sum ('G' f)) + ((- f) + f)
by A18, RLVECT_1:def 3
.=
(Sum ('G' f)) + (0. (Polynom-Ring INT.Ring))
by RLVECT_1:def 10
;
hence
( (Sum ('G' f)) - f = (Der1 INT.Ring) . (Sum ('G' f)) & (Sum ('G' f)) - f = (Der1 INT.Ring) . (Sum ('G' f)) & Sum ('G' f) = ((Der1 INT.Ring) . (Sum ('G' f))) + f )
by A18; verum