let a be Element of L; :: according to POLYALG1:def 1 :: thesis: for x, y being Element of (Formal-Series L) holds a * (x * y) = (a * x) * y
let x, y be Element of (Formal-Series L); :: thesis: a * (x * y) = (a * x) * y
reconsider x1 = x, y1 = y as Element of (Formal-Series L) ;
reconsider p = x1, q = y1 as sequence of L by Def2;
A1: a * x = a * p by Def2;
x * y = p *' q by Def2;
hence a * (x * y) = a * (p *' q) by Def2
.= (a * p) *' q by Th10
.= (a * x) * y by A1, Def2 ;
:: thesis: verum