let n be Ordinal; :: thesis: for L being non empty right-distributive doubleLoopStr
for p, q being Series of n,L
for a being Element of L holds a * (p + q) = (a * p) + (a * q)
let L be non empty right-distributive doubleLoopStr ; :: thesis: for p, q being Series of n,L
for a being Element of L holds a * (p + q) = (a * p) + (a * q)
let p1, p2 be Series of n,L; :: thesis: for a being Element of L holds a * (p1 + p2) = (a * p1) + (a * p2)
let b be Element of L; :: thesis: b * (p1 + p2) = (b * p1) + (b * p2)
set q1 = b * (p1 + p2);
set q2 = (b * p1) + (b * p2);

A1: now :: thesis: for x being object st x in dom (b * (p1 + p2)) holds
(b * (p1 + p2)) . x = ((b * p1) + (b * p2)) . x

let x be object ; :: thesis: ( x in dom (b * (p1 + p2)) implies (b * (p1 + p2)) . x = ((b * p1) + (b * p2)) . x )
assume x in dom (b * (p1 + p2)) ; :: thesis: (b * (p1 + p2)) . x = ((b * p1) + (b * p2)) . x
then reconsider u = x as bag of n ;
(b * (p1 + p2)) . u = b * ((p1 + p2) . u) by POLYNOM7:def 9
.= b * ((p1 . u) + (p2 . u)) by POLYNOM1:15
.= (b * (p1 . u)) + (b * (p2 . u)) by VECTSP_1:def 2
.= ((b * p1) . u) + (b * (p2 . u)) by POLYNOM7:def 9
.= ((b * p1) . u) + ((b * p2) . u) by POLYNOM7:def 9
.= ((b * p1) + (b * p2)) . u by POLYNOM1:15 ;
hence (b * (p1 + p2)) . x = ((b * p1) + (b * p2)) . x ; :: thesis: verum

end;

dom (b * (p1 + p2)) = Bags n by FUNCT_2:def 1
.= dom ((b * p1) + (b * p2)) by FUNCT_2:def 1 ;
hence b * (p1 + p2) = (b * p1) + (b * p2) by A1, FUNCT_1:2; :: thesis: verum