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);

.= 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

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

dom (b * (p1 + p2)) =
Bags n
by FUNCT_2:def 1
(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;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

.= 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