let n be Ordinal; :: thesis: for L being non empty right-distributive right_zeroed doubleLoopStr
for p, q being Series of n,L
for b being bag of n holds b *' (p + q) = (b *' p) + (b *' q)
let L be non empty right-distributive right_zeroed doubleLoopStr ; :: thesis: for p, q being Series of n,L
for b being bag of n holds b *' (p + q) = (b *' p) + (b *' q)
let p1, p2 be Series of n,L; :: thesis: for b being bag of n holds b *' (p1 + p2) = (b *' p1) + (b *' p2)
let b be bag of n; :: 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 ;

now :: thesis: ( ( b divides u & (b *' (p1 + p2)) . u = ((b *' p1) + (b *' p2)) . u ) or ( not b divides u & (b *' (p1 + p2)) . u = ((b *' p1) + (b *' p2)) . u ) )

per cases ( b divides u or not b divides u ) ;

case A2: b divides u ; :: thesis: (b *' (p1 + p2)) . u = ((b *' p1) + (b *' p2)) . u

hence (b *' (p1 + p2)) . u = (p1 + p2) . (u -' b) by POLYRED:def 1
.= (p1 . (u -' b)) + (p2 . (u -' b)) by POLYNOM1:15
.= ((b *' p1) . u) + (p2 . (u -' b)) by A2, POLYRED:def 1
.= ((b *' p1) . u) + ((b *' p2) . u) by A2, POLYRED:def 1
.= ((b *' p1) + (b *' p2)) . u by POLYNOM1:15 ;
:: thesis: verum

end;

case A3: not b divides u ; :: thesis: (b *' (p1 + p2)) . u = ((b *' p1) + (b *' p2)) . u

hence (b *' (p1 + p2)) . u = 0. L by POLYRED:def 1
.= (0. L) + (0. L) by RLVECT_1:def 4
.= ((b *' p1) . u) + (0. L) by A3, POLYRED:def 1
.= ((b *' p1) . u) + ((b *' p2) . u) by A3, POLYRED:def 1
.= ((b *' p1) + (b *' p2)) . u by POLYNOM1:15 ;
:: thesis: verum

end;

end;

end;

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