let R be domRing; for p, q being Polynomial of R st p = anpoly ((1. R),1) holds
for i being Element of NAT holds
( (p *' q) . (i + 1) = q . i & (p *' q) . 0 = 0. R )
let p, q be Polynomial of R; ( p = anpoly ((1. R),1) implies for i being Element of NAT holds
( (p *' q) . (i + 1) = q . i & (p *' q) . 0 = 0. R ) )
assume A1:
p = anpoly ((1. R),1)
; for i being Element of NAT holds
( (p *' q) . (i + 1) = q . i & (p *' q) . 0 = 0. R )
reconsider pq = p *' q as Polynomial of R ;
A2:
for i being Element of NAT holds (p *' q) . (i + 1) = q . i
proof
let i be
Element of
NAT ;
(p *' q) . (i + 1) = q . i
consider FGi being
FinSequence of the
carrier of
R such that A3:
len FGi = (i + 1) + 1
and A4:
(p *' q) . (i + 1) = Sum FGi
and A5:
for
k being
Element of
NAT st
k in dom FGi holds
FGi . k = (p . (k -' 1)) * (q . ((i + 2) -' k))
by POLYNOM3:def 9;
A6:
dom FGi = Seg (i + 2)
by A3, FINSEQ_1:def 3;
A7:
dom FGi = Seg (i + 2)
by A3, FINSEQ_1:def 3;
A8:
2
-' 1
= 2
- 1
by XREAL_1:233;
A9:
p . 0 = 0. R
by A1, POLYDIFF:25;
1
<= (i + 1) + 1
by NAT_1:11;
then A11:
1
in dom FGi
by A6;
then A12:
FGi /. 1 =
FGi . 1
by PARTFUN1:def 6
.=
(p . (1 -' 1)) * (q . ((i + 2) -' 1))
by A5, A11
.=
(0. R) * (q . ((i + 2) -' 1))
by A9, XREAL_1:232
.=
0. R
;
A13:
p . 1
= 1. R
by A1, POLYDIFF:24;
2
<= i + 2
by NAT_1:11;
then
2
in Seg (i + 2)
;
then A14:
2
in dom FGi
by A3, FINSEQ_1:def 3;
then A15:
FGi /. 2 =
FGi . 2
by PARTFUN1:def 6
.=
(p . 1) * (q . ((i + 2) -' 2))
by A8, A5, A14
.=
q . i
by A13, NAT_D:34
;
A16:
not
FGi is
empty
by A3;
set FGi1 =
FGi /^ 1;
reconsider e = 1 as
Nat ;
A17:
FGi | e =
<*(FGi . 1)*>
by A16, FINSEQ_5:20
.=
<*(FGi /. 1)*>
by A11, PARTFUN1:def 6
;
then A18:
i + 2 =
len (<*(FGi /. 1)*> ^ (FGi /^ 1))
by A3, RFINSEQ:8
.=
1
+ (len (FGi /^ 1))
by FINSEQ_5:8
;
then A19:
not
FGi /^ 1 is
empty
by NAT_1:11;
A20:
dom (FGi /^ 1) = Seg (i + 1)
by A18, FINSEQ_1:def 3;
A21:
1
<= i + 1
by NAT_1:11;
then A22:
1
in Seg (i + 1)
;
A23:
1
in dom (FGi /^ 1)
by A20, A21;
set FGi2 =
(FGi /^ 1) /^ 1;
A24:
(FGi /^ 1) | e =
<*((FGi /^ 1) . 1)*>
by A19, FINSEQ_5:20
.=
<*((FGi /^ 1) /. 1)*>
by A20, A22, PARTFUN1:def 6
;
then A25:
i + 1 =
len (<*((FGi /^ 1) /. 1)*> ^ ((FGi /^ 1) /^ 1))
by A18, RFINSEQ:8
.=
1
+ (len ((FGi /^ 1) /^ 1))
by FINSEQ_5:8
;
A26:
FGi /. 2 =
FGi . 2
by A14, PARTFUN1:def 6
.=
(<*(FGi /. 1)*> ^ (FGi /^ 1)) . (1 + 1)
by A17, RFINSEQ:8
.=
(FGi /^ 1) . 1
by A23, FINSEQ_3:103
.=
(FGi /^ 1) /. 1
by A23, PARTFUN1:def 6
;
A27:
Sum ((FGi /^ 1) /^ 1) = 0. R
proof
for
j being
Element of
NAT st
j in dom ((FGi /^ 1) /^ 1) holds
((FGi /^ 1) /^ 1) . j = 0. R
proof
let j be
Element of
NAT ;
( j in dom ((FGi /^ 1) /^ 1) implies ((FGi /^ 1) /^ 1) . j = 0. R )
assume A28:
j in dom ((FGi /^ 1) /^ 1)
;
((FGi /^ 1) /^ 1) . j = 0. R
dom ((FGi /^ 1) /^ 1) = Seg i
by A25, FINSEQ_1:def 3;
then A30:
(
j <= i & 1
<= j )
by A28, FINSEQ_1:1;
then A32:
j + 1
<= i + 1
by XREAL_1:6;
j + 1
>= 1
by NAT_1:11;
then A33:
j + 1
in dom (FGi /^ 1)
by A20, A32;
A34:
FGi . (j + 2) =
(<*(FGi /. 1)*> ^ (FGi /^ 1)) . ((j + 1) + 1)
by A17, RFINSEQ:8
.=
(FGi /^ 1) . (j + 1)
by A33, FINSEQ_3:103
.=
(<*((FGi /^ 1) /. 1)*> ^ ((FGi /^ 1) /^ 1)) . (j + 1)
by A24, RFINSEQ:8
.=
((FGi /^ 1) /^ 1) . j
by A28, FINSEQ_3:103
;
A35:
(j + 1) + 1
>= 1
+ 1
by NAT_1:11, XREAL_1:6;
then A36:
j + 2
>= 1
by XXREAL_0:2;
j + 2
<= i + 2
by A30, XREAL_1:6;
then A38:
j + 2
in dom FGi
by A7, A36;
j + 1
>= 1
+ 1
by A30, XREAL_1:6;
then
1
<> j + 1
;
then A40:
p . (j + 1) = 0. R
by A1, POLYDIFF:25;
A41:
(j + 2) -' 1 =
(j + 2) - 1
by A35, XXREAL_0:2, XREAL_1:233
.=
j + 1
;
FGi . (j + 2) =
(p . (j + 1)) * (q . ((i + 2) -' (j + 2)))
by A41, A5, A38
.=
0. R
by A40
;
hence
((FGi /^ 1) /^ 1) . j = 0. R
by A34;
verum
end;
hence
Sum ((FGi /^ 1) /^ 1) = 0. R
by POLYNOM3:1;
verum
end;
A42:
Sum FGi =
Sum (<*(FGi /. 1)*> ^ (FGi /^ 1))
by A17, RFINSEQ:8
.=
(FGi /. 1) + (Sum (FGi /^ 1))
by FVSUM_1:72
;
Sum (FGi /^ 1) =
Sum (<*((FGi /^ 1) /. 1)*> ^ ((FGi /^ 1) /^ 1))
by A24, RFINSEQ:8
.=
((FGi /^ 1) /. 1) + (Sum ((FGi /^ 1) /^ 1))
by FVSUM_1:72
;
hence
(p *' q) . (i + 1) = q . i
by A4, A27, A15, A26, A12, A42;
verum
end;
consider FG0 being FinSequence of the carrier of R such that
A44:
( len FG0 = 0 + 1 & (p *' q) . 0 = Sum FG0 & ( for k being Element of NAT st k in dom FG0 holds
FG0 . k = (p . (k -' 1)) * (q . ((0 + 1) -' k)) ) )
by POLYNOM3:def 9;
1 in Seg (len FG0)
by A44;
then
1 in dom FG0
by FINSEQ_1:def 3;
then FG0 . 1 =
(p . (1 -' 1)) * (q . ((0 + 1) -' 1))
by A44
.=
(p . 0) * (q . ((0 + 1) -' 1))
by NAT_D:34
.=
((anpoly ((1. R),1)) . 0) * (q . 0)
by A1, NAT_D:34
.=
(0. R) * (q . 0)
by POLYDIFF:25
;
then
FG0 = <*(0. R)*>
by FINSEQ_1:40, A44;
hence
for i being Element of NAT holds
( (p *' q) . (i + 1) = q . i & (p *' q) . 0 = 0. R )
by A2, A44, RLVECT_1:44; verum