let f, g be Polynomial of F_Complex ; :: thesis: (f *' g) *' = (f *' ) *' (g *' )
set h1 = f *' g;
A1: dom ((f *' g) *' ) = NAT by FUNCT_2:def 1
.= dom ((f *' ) *' (g *' )) by FUNCT_2:def 1 ;

now

let k' be set ; :: thesis: ( k' in dom ((f *' g) *' ) implies ((f *' g) *' ) . k' = ((f *' ) *' (g *' )) . k' )
assume k' in dom ((f *' g) *' ) ; :: thesis: ((f *' g) *' ) . k' = ((f *' ) *' (g *' )) . k'
then reconsider k = k' as Element of NAT ;
consider s being FinSequence of F_Complex such that
A2: ( len s = k + 1 & (f *' g) . k = Sum s & ( 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;
consider t being FinSequence of F_Complex such that
A3: ( len t = k + 1 & ((f *' ) *' (g *' )) . k = Sum t & ( 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;
A4: dom s = Seg (len t) by A2, A3, FINSEQ_1:def 3
.= dom t by FINSEQ_1:def 3 ;

A5: now

let j be Element of NAT ; :: thesis: ( j in dom t implies t . j = ((power F_Complex ) . (- (1_ F_Complex )),k) * ((s /. j) *' ) )
assume A6: j in dom t ; :: thesis: t . j = ((power F_Complex ) . (- (1_ F_Complex )),k) * ((s /. j) *' )
then j in Seg (len t) by FINSEQ_1:def 3;
then ( 1 <= j & j <= k + 1 ) by A3, FINSEQ_1:3;
then A7: ( (k + 1) - j >= j - j & j - 1 >= 1 - 1 ) by XREAL_1:11;
then A8: (j -' 1) + ((k + 1) -' j) = (j - 1) + ((k + 1) -' j) by XREAL_0:def 2
.= (j - 1) + ((k + 1) - j) by A7, XREAL_0:def 2
.= k ;
s . j = s /. j by A4, A6, PARTFUN1:def 8;
then A9: (s /. j) *' = ((f . (j -' 1)) * (g . ((k + 1) -' j))) *' by A2, A4, A6;
thus t . j = ((f *' ) . (j -' 1)) * ((g *' ) . ((k + 1) -' j)) by A3, A6
.= (((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 A8, Th3
.= ((power F_Complex ) . (- (1_ F_Complex )),k) * ((s /. j) *' ) by A9, COMPLFLD:90 ; :: thesis: verum

end;

defpred S₁[ set , set ] means $2 = (s /. $1) *' ;
A10: for j being Nat st j in Seg (len s) holds
ex x being Element of F_Complex st S₁[j,x] ;
consider u being FinSequence of F_Complex such that
A11: ( dom u = Seg (len s) & ( for j being Nat st j in Seg (len s) holds
S₁[j,u . j] ) ) from FINSEQ_1:sch 5(A10);
A12: ( len u = len s & ( for j being Element of NAT st j in dom u holds
u /. j = (s /. j) *' ) )

proof

thus len u = len s by A11, FINSEQ_1:def 3; :: thesis: for j being Element of NAT st j in dom u holds
u /. j = (s /. j) *'

now

let j be Element of NAT ; :: thesis: ( j in dom u implies u /. j = (s /. j) *' )
assume A13: j in dom u ; :: thesis: u /. j = (s /. j) *'
hence u /. j = u . j by PARTFUN1:def 8
.= (s /. j) *' by A11, A13 ;
:: thesis: verum

end;

hence for j being Element of NAT st j in dom u holds
u /. j = (s /. j) *' ; :: thesis: verum

end;

then A14: dom u = Seg (len t) by A2, A3, FINSEQ_1:def 3
.= dom t by FINSEQ_1:def 3 ;
A15: ((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;
A16: dom (((power F_Complex ) . (- (1_ F_Complex )),k) * u) = dom u by POLYNOM1:def 2;

now

let j be Nat; :: thesis: ( j in dom t implies (((power F_Complex ) . (- (1_ F_Complex )),k) * u) . j = t . j )
assume A17: j in dom t ; :: thesis: (((power F_Complex ) . (- (1_ F_Complex )),k) * u) . j = t . j
hence (((power F_Complex ) . (- (1_ F_Complex )),k) * u) . j = (((power F_Complex ) . (- (1_ F_Complex )),k) * u) /. j by A14, A16, PARTFUN1:def 8
.= ((power F_Complex ) . (- (1_ F_Complex )),k) * (u /. j) by A14, A17, POLYNOM1:def 2
.= ((power F_Complex ) . (- (1_ F_Complex )),k) * ((s /. j) *' ) by A12, A14, A17
.= t . j by A5, A17 ;
:: thesis: verum

end;

hence ((power F_Complex ) . (- (1_ F_Complex )),k) * u = t by A14, A16, FINSEQ_1:17; :: thesis: verum

end;

Sum u = (Sum s) *' by A12, Th6;
then ((f *' g) *' ) . k = ((power F_Complex ) . (- (1_ F_Complex )),k) * (Sum u) by A2, Def9
.= ((f *' ) *' (g *' )) . k by A3, A15, Th8 ;
hence ((f *' g) *' ) . k' = ((f *' ) *' (g *' )) . k' ; :: thesis: verum

end;

hence (f *' g) *' = (f *' ) *' (g *' ) by A1, FUNCT_1:9; :: thesis: verum