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

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