let R be non degenerated comRing; for f, g being Series of 1,R holds (f *' g) * NBag1 = (f * NBag1) *' (g * NBag1)
let f, g be Series of 1,R; (f *' g) * NBag1 = (f * NBag1) *' (g * NBag1)
for o being object st o in NAT holds
((f *' g) * NBag1) . o = ((f * NBag1) *' (g * NBag1)) . o
proof
let o be
object ;
( o in NAT implies ((f *' g) * NBag1) . o = ((f * NBag1) *' (g * NBag1)) . o )
assume A1:
o in NAT
;
((f *' g) * NBag1) . o = ((f * NBag1) *' (g * NBag1)) . o
then reconsider m =
o as
Element of
NAT ;
A2:
NBag1 . o = 1
--> m
by Def1;
reconsider b =
NBag1 . o as
Element of
Bags 1
by A2, PRE_POLY:def 12;
A3:
0 in 1
by CARD_1:49, TARSKI:def 1;
then A4:
b . 0 = m
by A2, FUNCOP_1:7;
set F =
NBag1 | (Segm ((b . 0) + 1));
consider s being
FinSequence of the
carrier of
R such that A5:
(
(f *' g) . b = Sum s &
len s = len (decomp b) & ( for
k being
Element of
NAT st
k in dom s holds
ex
b1,
b2 being
bag of 1 st
(
(decomp b) /. k = <*b1,b2*> &
s /. k = (f . b1) * (g . b2) ) ) )
by POLYNOM1:def 10;
A6:
((f *' g) * NBag1) . o =
(f *' g) . b
by A1, FUNCT_2:15
.=
Sum s
by A5
;
consider r being
FinSequence of the
carrier of
R such that A7:
(
len r = m + 1 &
((f * NBag1) *' (g * NBag1)) . m = Sum r & ( for
k being
Element of
NAT st
k in dom r holds
r . k = ((f * NBag1) . (k -' 1)) * ((g * NBag1) . ((m + 1) -' k)) ) )
by POLYNOM3:def 9;
A8:
Seg (len (decomp b)) =
dom (decomp b)
by FINSEQ_1:def 3
.=
dom (divisors b)
by PRE_POLY:def 17
.=
Seg (len (divisors b))
by FINSEQ_1:def 3
;
then
len (decomp b) = len (divisors b)
by FINSEQ_1:6;
then A9:
len s =
(b . 0) + 1
by A5, Th15
.=
len r
by A2, A3, FUNCOP_1:7, A7
;
A10:
dom (decomp b) =
Seg (len (decomp b))
by FINSEQ_1:def 3
.=
Seg ((b . 0) + 1)
by A8, Th15
;
A11:
dom (decomp b) =
Seg (len s)
by A5, FINSEQ_1:def 3
.=
dom s
by FINSEQ_1:def 3
;
for
k being
Nat st 1
<= k &
k <= len s holds
s . k = r . k
proof
let k be
Nat;
( 1 <= k & k <= len s implies s . k = r . k )
assume A12:
( 1
<= k &
k <= len s )
;
s . k = r . k
then A13:
k in Seg (len s)
;
A14:
k in dom s
by A12, FINSEQ_3:25;
then consider b1,
b2 being
bag of 1
such that A15:
(
(decomp b) /. k = <*b1,b2*> &
s /. k = (f . b1) * (g . b2) )
by A5;
A16:
(
k in dom (decomp b) &
(decomp b) /. k = <*b1,b2*> )
by A13, FINSEQ_1:def 3, A11, A15;
then
b1 = (divisors b) /. k
by PRE_POLY:70;
then A17:
<*b1,(b -' b1)*> =
(decomp b) /. k
by A16, PRE_POLY:def 17
.=
<*b1,b2*>
by A15
;
dom (decomp b) =
Seg (len (divisors b))
by A8, FINSEQ_1:def 3
.=
dom (divisors b)
by FINSEQ_1:def 3
.=
dom (XFS2FS (NBag1 | (Segm ((b . 0) + 1))))
by Th25
;
then A18:
k in dom (XFS2FS (NBag1 | (Segm ((b . 0) + 1))))
by A13, FINSEQ_1:def 3, A11;
A19:
k in Seg ((b . 0) + 1)
by A13, FINSEQ_1:def 3, A11, A10;
then A20:
( 1
<= k &
k <= len (NBag1 | (Segm ((b . 0) + 1))) )
by FINSEQ_1:1;
then reconsider k1 =
k - 1 as
Element of
NAT by INT_1:3;
A21:
( 1
<= k &
k <= (b . 0) + 1 )
by A19, FINSEQ_1:1;
k - 1
< k - 0
by XREAL_1:10;
then A22:
k - 1
< (b . 0) + 1
by A21, XXREAL_0:2;
then A23:
k1 in dom (NBag1 | (Segm ((b . 0) + 1)))
by NAT_1:44;
A24:
b1 =
(divisors b) /. k
by PRE_POLY:70, A16
.=
(XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) /. k
by Th25
.=
(XFS2FS (NBag1 | (Segm ((b . 0) + 1)))) . k
by A18, PARTFUN1:def 6
.=
(NBag1 | (Segm ((b . 0) + 1))) . (k - 1)
by A20, AFINSQ_1:def 9
.=
NBag1 . k1
by A23, FUNCT_1:47
.=
1
--> k1
by Def1
;
A25:
0 in 1
by CARD_1:49, TARSKI:def 1;
aaa:
k -' 1
= k - 1
by A21, XREAL_0:def 2;
then A26:
b . 0 >= k - 1
by A22, NAT_1:13;
A27:
(b . 0) -' (k -' 1) =
(b . 0) -' (k - 1)
by A21, XREAL_0:def 2
.=
(b . 0) - (k - 1)
by A26, XREAL_1:233
.=
((b . 0) + 1) - k
.=
((b . 0) + 1) -' k
by A21, XREAL_1:233
;
A28:
b2 =
b -' b1
by A17, FINSEQ_1:77
.=
1
--> ((b . 0) -' (b1 . 0))
by Th7
.=
1
--> (((b . 0) + 1) -' k)
by aaa, A27, A25, A24, FUNCOP_1:7
;
A29:
(f * NBag1) . (k - 1) =
f . (NBag1 . k1)
by FUNCT_2:15
.=
f . b1
by Def1, A24
;
A30:
(g * NBag1) . (((b . 0) + 1) -' k) =
g . (NBag1 . (((b . 0) + 1) -' k))
by FUNCT_2:15
.=
g . b2
by A28, Def1
;
k in dom r
by A9, A13, FINSEQ_1:def 3;
then r . k =
((f * NBag1) . (k -' 1)) * ((g * NBag1) . (((b . 0) + 1) -' k))
by A4, A7
.=
(f . b1) * (g . b2)
by aaa, A29, A30
.=
s . k
by A14, A15, PARTFUN1:def 6
;
hence
s . k = r . k
;
verum
end;
then
s = r
by A9;
then ((f *' g) * NBag1) . o =
Sum r
by A6
.=
((f * NBag1) *' (g * NBag1)) . o
by A7
;
hence
((f *' g) * NBag1) . o = ((f * NBag1) *' (g * NBag1)) . o
;
verum
end;
hence
(f *' g) * NBag1 = (f * NBag1) *' (g * NBag1)
; verum