let L be non empty right_complementable distributive add-associative right_zeroed associative commutative doubleLoopStr ; for p1, p2 being Polynomial of L
for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)
let p1, p2 be Polynomial of L; for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)
let x be Element of L; p1 *' (x * p2) = x * (p1 *' p2)
set f = p1 *' (x * p2);
set g = x * (p1 *' p2);
A1:
now for i9 being object st i9 in dom (p1 *' (x * p2)) holds
(p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9let i9 be
object ;
( i9 in dom (p1 *' (x * p2)) implies (p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9 )assume
i9 in dom (p1 *' (x * p2))
;
(p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9then reconsider i =
i9 as
Element of
NAT ;
consider rf being
FinSequence of
L such that A2:
len rf = i + 1
and A3:
(p1 *' (x * p2)) . i = Sum rf
and A4:
for
k being
Element of
NAT st
k in dom rf holds
rf . k = (p1 . (k -' 1)) * ((x * p2) . ((i + 1) -' k))
by POLYNOM3:def 9;
consider rp being
FinSequence of
L such that A5:
len rp = i + 1
and A6:
(p1 *' p2) . i = Sum rp
and A7:
for
k being
Element of
NAT st
k in dom rp holds
rp . k = (p1 . (k -' 1)) * (p2 . ((i + 1) -' k))
by POLYNOM3:def 9;
A8:
Seg (len (x * rp)) =
dom (x * rp)
by FINSEQ_1:def 3
.=
dom rp
by POLYNOM1:def 1
.=
Seg (len rp)
by FINSEQ_1:def 3
;
then A9:
dom (x * rp) =
Seg (len rf)
by A2, A5, FINSEQ_1:def 3
.=
dom rf
by FINSEQ_1:def 3
;
A10:
dom (x * rp) = dom rp
by POLYNOM1:def 1;
A11:
now for j being Nat st 1 <= j & j <= len rf holds
(x * rp) . j = rf . jlet j be
Nat;
( 1 <= j & j <= len rf implies (x * rp) . j = rf . j )assume that A12:
1
<= j
and A13:
j <= len rf
;
(x * rp) . j = rf . jA14:
j in dom rf
by A12, A13, FINSEQ_3:25;
then A15:
rp /. j = rp . j
by A9, A10, PARTFUN1:def 6;
thus (x * rp) . j =
(x * rp) /. j
by A9, A14, PARTFUN1:def 6
.=
x * (rp /. j)
by A9, A10, A14, POLYNOM1:def 1
.=
x * ((p1 . (j -' 1)) * (p2 . ((i + 1) -' j)))
by A7, A9, A10, A14, A15
.=
(p1 . (j -' 1)) * (x * (p2 . ((i + 1) -' j)))
by GROUP_1:def 3
.=
(p1 . (j -' 1)) * ((x * p2) . ((i + 1) -' j))
by POLYNOM5:def 4
.=
rf . j
by A4, A14
;
verum end; (x * (p1 *' p2)) . i =
x * (Sum rp)
by A6, POLYNOM5:def 4
.=
Sum (x * rp)
by Th8
.=
(p1 *' (x * p2)) . i
by A2, A3, A5, A8, A11, FINSEQ_1:6, FINSEQ_1:14
;
hence
(p1 *' (x * p2)) . i9 = (x * (p1 *' p2)) . i9
;
verum end;
dom (p1 *' (x * p2)) =
NAT
by FUNCT_2:def 1
.=
dom (x * (p1 *' p2))
by FUNCT_2:def 1
;
hence
p1 *' (x * p2) = x * (p1 *' p2)
by A1, FUNCT_1:2; verum