let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non empty ZeroStr
for p being Series of n,L
for b1, b2 being bag of holds (b1 + b2) *' p = b1 *' (b2 *' p)
let T be connected TermOrder of n; :: thesis: for L being non empty ZeroStr
for p being Series of n,L
for b1, b2 being bag of holds (b1 + b2) *' p = b1 *' (b2 *' p)
let L be non empty ZeroStr ; :: thesis: for p being Series of n,L
for b1, b2 being bag of holds (b1 + b2) *' p = b1 *' (b2 *' p)
let p be Series of n,L; :: thesis: for b1, b2 being bag of holds (b1 + b2) *' p = b1 *' (b2 *' p)
let b1, b2 be bag of ; :: thesis: (b1 + b2) *' p = b1 *' (b2 *' p)
set q = (b1 + b2) *' p;
set r = b1 *' (b2 *' p);
A1: dom ((b1 + b2) *' p) = Bags n by FUNCT_2:def 1
.= dom (b1 *' (b2 *' p)) by FUNCT_2:def 1 ;

now

let u be set ; :: thesis: ( u in dom ((b1 + b2) *' p) implies ((b1 + b2) *' p) . u = (b1 *' (b2 *' p)) . u )
assume u in dom ((b1 + b2) *' p) ; :: thesis: ((b1 + b2) *' p) . u = (b1 *' (b2 *' p)) . u
then reconsider b = u as bag of by POLYNOM1:def 14;

now

per cases ( b1 + b2 divides b or not b1 + b2 divides b ) ;

case A2: b1 + b2 divides b ; :: thesis: (b1 *' (b2 *' p)) . b = ((b1 + b2) *' p) . b

then consider b3 being bag of such that
A3: (b1 + b2) + b3 = b by TERMORD:1;
A4: ( b1 + (b2 + b3) = b & b2 + (b1 + b3) = b ) by A3, POLYNOM1:39;
then ( b1 divides b & b2 divides b ) by TERMORD:1;
then A5: (b1 *' (b2 *' p)) . b = (b2 *' p) . (b -' b1) by Def1;
b2 + b3 = b -' b1 by A4, POLYNOM1:52;
then b2 divides b -' b1 by TERMORD:1;
hence (b1 *' (b2 *' p)) . b = p . ((b -' b1) -' b2) by A5, Def1
.= p . (b -' (b1 + b2)) by POLYNOM1:40
.= ((b1 + b2) *' p) . b by A2, Def1 ;
:: thesis: verum

end;

case A6: not b1 + b2 divides b ; :: thesis: ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b

then A7: ((b1 + b2) *' p) . b = 0. L by Def1;

now

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

case A8: b1 divides b ; :: thesis: ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b

then A9: (b1 *' (b2 *' p)) . b = (b2 *' p) . (b -' b1) by Def1;

now

assume b2 divides b -' b1 ; :: thesis: contradiction
then ((b -' b1) -' b2) + b2 = b -' b1 by POLYNOM1:51;
then (((b -' b1) -' b2) + b2) + b1 = b by A8, POLYNOM1:51;
then ((b -' b1) -' b2) + (b2 + b1) = b by POLYNOM1:39;
hence contradiction by A6, TERMORD:1; :: thesis: verum

end;

hence ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b by A7, A9, Def1; :: thesis: verum

end;

case not b1 divides b ; :: thesis: ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b

hence ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b by A7, Def1; :: thesis: verum

end;

end;

end;

hence ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b ; :: thesis: verum

end;

end;

end;

hence ((b1 + b2) *' p) . u = (b1 *' (b2 *' p)) . u ; :: thesis: verum

end;

hence (b1 + b2) *' p = b1 *' (b2 *' p) by A1, FUNCT_1:9; :: thesis: verum