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
.= ((b *' p1) . u) + ((b *' p2) . u) by
.= ((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
.= ((b *' p1) . u) + ((b *' p2) . u) by
.= ((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 ; :: thesis: verum