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 n 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 n 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 n holds (b1 + b2) *' p = b1 *' (b2 *' p)
let p be Series of n,L; :: thesis: for b1, b2 being bag of n holds (b1 + b2) *' p = b1 *' (b2 *' p)
let b1, b2 be bag of n; :: thesis: (b1 + b2) *' p = b1 *' (b2 *' p)
set q = (b1 + b2) *' p;
set r = b1 *' (b2 *' p);
A1: now :: thesis: for u being object st u in dom ((b1 + b2) *' p) holds
((b1 + b2) *' p) . u = (b1 *' (b2 *' p)) . u
let u be object ; :: 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 n ;
now :: thesis: ( ( b1 + b2 divides b & (b1 *' (b2 *' p)) . b = ((b1 + b2) *' p) . b ) or ( not b1 + b2 divides b & ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b ) )
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 n such that
A3: (b1 + b2) + b3 = b by TERMORD:1;
A4: b1 + (b2 + b3) = b by A3, PRE_POLY:35;
then b2 + b3 = b -' b1 by PRE_POLY:48;
then A5: b2 divides b -' b1 by TERMORD:1;
b1 divides b by A4, TERMORD:1;
then (b1 *' (b2 *' p)) . b = (b2 *' p) . (b -' b1) by Def1;
hence (b1 *' (b2 *' p)) . b = p . ((b -' b1) -' b2) by A5, Def1
.= p . (b -' (b1 + b2)) by PRE_POLY:36
.= ((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 :: thesis: ( ( b1 divides b & ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b ) or ( not b1 divides b & ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b ) )
per cases ( b1 divides b or not b1 divides b ) ;
case A8: b1 divides b ; :: thesis: ((b1 + b2) *' p) . b = (b1 *' (b2 *' p)) . b
A9: now :: thesis: not b2 divides b -' b1
assume b2 divides b -' b1 ; :: thesis: contradiction
then ((b -' b1) -' b2) + b2 = b -' b1 by PRE_POLY:47;
then (((b -' b1) -' b2) + b2) + b1 = b by A8, PRE_POLY:47;
then ((b -' b1) -' b2) + (b2 + b1) = b by PRE_POLY:35;
hence contradiction by A6, TERMORD:1; :: thesis: verum
end;
(b1 *' (b2 *' p)) . b = (b2 *' p) . (b -' b1) by A8, Def1;
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;
dom ((b1 + b2) *' p) = Bags n by FUNCT_2:def 1
.= dom (b1 *' (b2 *' p)) by FUNCT_2:def 1 ;
hence (b1 + b2) *' p = b1 *' (b2 *' p) by A1, FUNCT_1:2; :: thesis: verum