let n be Ordinal; :: thesis: for L being non degenerated comRing holds Formal-Series (n,L) is mix-associative
let L be non degenerated comRing; :: thesis: Formal-Series (n,L) is mix-associative
for a being Element of L
for x, y being Element of (Formal-Series (n,L)) holds a * (x * y) = (a * x) * y

proof

let a be Element of L; :: thesis: for x, y being Element of (Formal-Series (n,L)) holds a * (x * y) = (a * x) * y
for x, y being Element of (Formal-Series (n,L)) holds a * (x * y) = (a * x) * y

proof

let x, y be Element of (Formal-Series (n,L)); :: thesis: a * (x * y) = (a * x) * y
reconsider x1 = x, y1 = y as Element of (Formal-Series (n,L)) ;
reconsider p = x1, q = y1 as Series of n,L by Def3;
A1: a * x = a * p by Def3;
x * y = p *' q by Def3;
hence a * (x * y) = a * (p *' q) by Def3
.= (a * p) *' q by POLYRED:12
.= (a * x) * y by A1, Def3 ;
:: thesis: verum

end;

hence for x, y being Element of (Formal-Series (n,L)) holds a * (x * y) = (a * x) * y ; :: thesis: verum

end;

hence Formal-Series (n,L) is mix-associative by POLYALG1:def 1; :: thesis: verum