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

let x be set ; :: 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 10
.= b * ((p1 . u) + (p2 . u)) by POLYNOM1:def 21
.= (b * (p1 . u)) + (b * (p2 . u)) by VECTSP_1:def 11
.= ((b * p1) . u) + (b * (p2 . u)) by POLYNOM7:def 10
.= ((b * p1) . u) + ((b * p2) . u) by POLYNOM7:def 10
.= ((b * p1) + (b * p2)) . u by POLYNOM1:def 21 ;
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:9; :: thesis: verum