let a be Element of ; :: according to POLYALG1:def 1 :: thesis: for x, y being Element of holds a * (x * y) = (a * x) * y
let x, y be Element of ; :: thesis: a * (x * y) = (a * x) * y
reconsider x1 = x, y1 = y as Element of ;
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