let L be non empty right_complementable associative commutative distributive add-associative right_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: for x being Element of L holds p1 *' (x * p2) = x * (p1 *' p2)
let x be Element of L; :: thesis: p1 *' (x * p2) = x * (p1 *' p2)
set f = p1 *' (x * p2);
set g = x * (p1 *' p2);
A1: dom (p1 *' (x * p2)) =
NAT
by FUNCT_2:def 1
.=
dom (x * (p1 *' p2))
by FUNCT_2:def 1
;
now let i' be
set ;
:: thesis: ( i' in dom (p1 *' (x * p2)) implies (p1 *' (x * p2)) . i' = (x * (p1 *' p2)) . i' )assume
i' in dom (p1 *' (x * p2))
;
:: thesis: (p1 *' (x * p2)) . i' = (x * (p1 *' p2)) . i'then reconsider i =
i' as
Element of
NAT ;
consider rf being
FinSequence of
L such that A2:
(
len rf = i + 1 &
(p1 *' (x * p2)) . i = Sum rf & ( 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 11;
consider rp being
FinSequence of
L such that A3:
(
len rp = i + 1 &
(p1 *' p2) . i = Sum rp & ( for
k being
Element of
NAT st
k in dom rp holds
rp . k = (p1 . (k -' 1)) * (p2 . ((i + 1) -' k)) ) )
by POLYNOM3:def 11;
A4:
Seg (len (x * rp)) =
dom (x * rp)
by FINSEQ_1:def 3
.=
dom rp
by POLYNOM1:def 2
.=
Seg (len rp)
by FINSEQ_1:def 3
;
then A5:
len (x * rp) = len rf
by A2, A3, FINSEQ_1:8;
A6:
dom (x * rp) =
Seg (len rf)
by A2, A3, A4, FINSEQ_1:def 3
.=
dom rf
by FINSEQ_1:def 3
;
A7:
dom (x * rp) = dom rp
by POLYNOM1:def 2;
A8:
now let j be
Nat;
:: thesis: ( 1 <= j & j <= len rf implies (x * rp) . j = rf . j )assume
( 1
<= j &
j <= len rf )
;
:: thesis: (x * rp) . j = rf . jthen A9:
j in dom rf
by FINSEQ_3:27;
then A10:
rp /. j = rp . j
by A6, A7, PARTFUN1:def 8;
thus (x * rp) . j =
(x * rp) /. j
by A6, A9, PARTFUN1:def 8
.=
x * (rp /. j)
by A6, A7, A9, POLYNOM1:def 2
.=
x * ((p1 . (j -' 1)) * (p2 . ((i + 1) -' j)))
by A3, A6, A7, A9, A10
.=
(p1 . (j -' 1)) * (x * (p2 . ((i + 1) -' j)))
by GROUP_1:def 4
.=
(p1 . (j -' 1)) * ((x * p2) . ((i + 1) -' j))
by POLYNOM5:def 3
.=
rf . j
by A2, A9
;
:: thesis: verum end; (x * (p1 *' p2)) . i =
x * (Sum rp)
by A3, POLYNOM5:def 3
.=
Sum (x * rp)
by Th8
.=
(p1 *' (x * p2)) . i
by A2, A5, A8, FINSEQ_1:18
;
hence
(p1 *' (x * p2)) . i' = (x * (p1 *' p2)) . i'
;
:: thesis: verum end;
hence
p1 *' (x * p2) = x * (p1 *' p2)
by A1, FUNCT_1:9; :: thesis: verum