let L be non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p1, p2 being Polynomial of L
for p2' being Element of (Polynom-Ring L) st p2' = p2 holds
for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p2' * F)
let p1, p2 be Polynomial of L; :: thesis: for p2' being Element of (Polynom-Ring L) st p2' = p2 holds
for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p2' * F)
let p2' be Element of (Polynom-Ring L); :: thesis: ( p2' = p2 implies for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p2' * F) )
assume A1: p2' = p2 ; :: thesis: for F being FinSequence of (Polynom-Ring L) st p1 = Sum F holds
p2 *' p1 = Sum (p2' * F)
let F be FinSequence of (Polynom-Ring L); :: thesis: ( p1 = Sum F implies p2 *' p1 = Sum (p2' * F) )
assume A2: p1 = Sum F ; :: thesis: p2 *' p1 = Sum (p2' * F)
reconsider p1' = p1 as Element of (Polynom-Ring L) by POLYNOM3:def 12;
p2' * p1' = Sum (p2' * F) by A2, Th8;
hence p2 *' p1 = Sum (p2' * F) by A1, POLYNOM3:def 12; :: thesis: verum