let f, g be Polynomial of F_Complex; (f *' g) *' = (f *') *' (g *')
set h1 = f *' g;
A1:
now for k9 being object st k9 in dom ((f *' g) *') holds
((f *' g) *') . k9 = ((f *') *' (g *')) . k9let k9 be
object ;
( k9 in dom ((f *' g) *') implies ((f *' g) *') . k9 = ((f *') *' (g *')) . k9 )assume
k9 in dom ((f *' g) *')
;
((f *' g) *') . k9 = ((f *') *' (g *')) . k9then reconsider k =
k9 as
Element of
NAT ;
consider s being
FinSequence of
F_Complex such that A2:
len s = k + 1
and A3:
(f *' g) . k = Sum s
and A4:
for
j being
Element of
NAT st
j in dom s holds
s . j = (f . (j -' 1)) * (g . ((k + 1) -' j))
by POLYNOM3:def 9;
defpred S1[
set ,
set ]
means $2
= (s /. $1) *' ;
consider t being
FinSequence of
F_Complex such that A5:
len t = k + 1
and A6:
((f *') *' (g *')) . k = Sum t
and A7:
for
j being
Element of
NAT st
j in dom t holds
t . j = ((f *') . (j -' 1)) * ((g *') . ((k + 1) -' j))
by POLYNOM3:def 9;
A8:
for
j being
Nat st
j in Seg (len s) holds
ex
x being
Element of
F_Complex st
S1[
j,
x]
;
consider u being
FinSequence of
F_Complex such that A9:
(
dom u = Seg (len s) & ( for
j being
Nat st
j in Seg (len s) holds
S1[
j,
u . j] ) )
from FINSEQ_1:sch 5(A8);
A12:
dom u =
Seg (len t)
by A2, A5, A9
.=
dom t
by FINSEQ_1:def 3
;
A13:
dom s =
Seg (len t)
by A2, A5, FINSEQ_1:def 3
.=
dom t
by FINSEQ_1:def 3
;
A14:
now for j being Element of NAT st j in dom t holds
t . j = ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *')let j be
Element of
NAT ;
( j in dom t implies t . j = ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *') )assume A15:
j in dom t
;
t . j = ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *')then
s . j = s /. j
by A13, PARTFUN1:def 6;
then A16:
(s /. j) *' = ((f . (j -' 1)) * (g . ((k + 1) -' j))) *'
by A4, A13, A15;
A17:
j in Seg (len t)
by A15, FINSEQ_1:def 3;
then
j <= k + 1
by A5, FINSEQ_1:1;
then A18:
(k + 1) - j >= j - j
by XREAL_1:9;
1
<= j
by A17, FINSEQ_1:1;
then
j - 1
>= 1
- 1
by XREAL_1:9;
then A19:
(j -' 1) + ((k + 1) -' j) =
(j - 1) + ((k + 1) -' j)
by XREAL_0:def 2
.=
(j - 1) + ((k + 1) - j)
by A18, XREAL_0:def 2
.=
k
;
thus t . j =
((f *') . (j -' 1)) * ((g *') . ((k + 1) -' j))
by A7, A15
.=
(((power F_Complex) . ((- (1_ F_Complex)),(j -' 1))) * ((f . (j -' 1)) *')) * ((g *') . ((k + 1) -' j))
by Def9
.=
(((power F_Complex) . ((- (1_ F_Complex)),(j -' 1))) * ((f . (j -' 1)) *')) * (((power F_Complex) . ((- (1_ F_Complex)),((k + 1) -' j))) * ((g . ((k + 1) -' j)) *'))
by Def9
.=
(((power F_Complex) . ((- (1_ F_Complex)),(j -' 1))) * ((power F_Complex) . ((- (1_ F_Complex)),((k + 1) -' j)))) * (((f . (j -' 1)) *') * ((g . ((k + 1) -' j)) *'))
.=
((power F_Complex) . ((- (1_ F_Complex)),k)) * (((f . (j -' 1)) *') * ((g . ((k + 1) -' j)) *'))
by A19, Th3
.=
((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *')
by A16, COMPLFLD:54
;
verum end; A20:
((power F_Complex) . ((- (1_ F_Complex)),k)) * u = t
proof
set b =
(power F_Complex) . (
(- (1_ F_Complex)),
k);
set a =
((power F_Complex) . ((- (1_ F_Complex)),k)) * u;
A21:
dom (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) = dom u
by POLYNOM1:def 1;
now for j being Nat st j in dom t holds
(((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j = t . jlet j be
Nat;
( j in dom t implies (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j = t . j )assume A22:
j in dom t
;
(((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j = t . jhence (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j =
(((power F_Complex) . ((- (1_ F_Complex)),k)) * u) /. j
by A12, A21, PARTFUN1:def 6
.=
((power F_Complex) . ((- (1_ F_Complex)),k)) * (u /. j)
by A12, A22, POLYNOM1:def 1
.=
((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *')
by A10, A12, A22
.=
t . j
by A14, A22
;
verum end;
hence
((power F_Complex) . ((- (1_ F_Complex)),k)) * u = t
by A12, A21, FINSEQ_1:13;
verum
end;
len u = len s
by A9, FINSEQ_1:def 3;
then
Sum u = (Sum s) *'
by A10, Th6;
then ((f *' g) *') . k =
((power F_Complex) . ((- (1_ F_Complex)),k)) * (Sum u)
by A3, Def9
.=
((f *') *' (g *')) . k
by A6, A20, Th8
;
hence
((f *' g) *') . k9 = ((f *') *' (g *')) . k9
;
verum end;
dom ((f *' g) *') =
NAT
by FUNCT_2:def 1
.=
dom ((f *') *' (g *'))
by FUNCT_2:def 1
;
hence
(f *' g) *' = (f *') *' (g *')
by A1, FUNCT_1:2; verum