let f, g be Polynomial of F_Complex ; (f *' g) *' = (f *' ) *' (g *' )
set h1 = f *' g;
A1:
now let k9 be
set ;
( 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 11;
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 11;
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 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 8;
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:3;
then A18:
(k + 1) - j >= j - j
by XREAL_1:11;
1
<= j
by A17, FINSEQ_1:3;
then
j - 1
>= 1
- 1
by XREAL_1:11;
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:90
;
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 2;
now let 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 8
.=
((power F_Complex ) . (- (1_ F_Complex )),k) * (u /. j)
by A12, A22, POLYNOM1:def 2
.=
((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:17;
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:9; verum