let f, g be Polynomial of F_Complex; :: thesis: (f *' g) *' = (f *') *' (g *')
set h1 = f *' g;

A1: now :: thesis: for k9 being object st k9 in dom ((f *' g) *') holds
((f *' g) *') . k9 = ((f *') *' (g *')) . k9

let k9 be object ; :: thesis: ( k9 in dom ((f *' g) *') implies ((f *' g) *') . k9 = ((f *') *' (g *')) . k9 )
assume k9 in dom ((f *' g) *') ; :: thesis: ((f *' g) *') . k9 = ((f *') *' (g *')) . k9
then 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 S₁[ 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 S₁[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
S₁[j,u . j] ) ) from FINSEQ_1:sch 5(A8);

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

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

end;

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 :: thesis: 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 ; :: thesis: ( j in dom t implies t . j = ((power F_Complex) . ((- (1_ F_Complex)),k)) * ((s /. j) *') )
assume A15: j in dom t ; :: thesis: 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 ; :: thesis: 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 :: thesis: for j being Nat st j in dom t holds
(((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j = t . j

let j be Nat; :: thesis: ( j in dom t implies (((power F_Complex) . ((- (1_ F_Complex)),k)) * u) . j = t . j )
assume A22: 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 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 ;
:: thesis: verum

end;

hence ((power F_Complex) . ((- (1_ F_Complex)),k)) * u = t by A12, A21, FINSEQ_1:13; :: thesis: 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 ; :: thesis: 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; :: thesis: verum