let A, B be set ; :: thesis: for b being Rbag of
for b1 being Rbag of
for b2 being Rbag of st b = b1 +* b2 holds
Sum b = (Sum b1) + (Sum b2)
let b be Rbag of ; :: thesis: for b1 being Rbag of
for b2 being Rbag of st b = b1 +* b2 holds
Sum b = (Sum b1) + (Sum b2)
let b1 be Rbag of ; :: thesis: for b2 being Rbag of st b = b1 +* b2 holds
Sum b = (Sum b1) + (Sum b2)
let b2 be Rbag of ; :: thesis: ( b = b1 +* b2 implies Sum b = (Sum b1) + (Sum b2) )
assume A1: b = b1 +* b2 ; :: thesis: Sum b = (Sum b1) + (Sum b2)
set B1 = (EmptyBag A) +* b1;
set B2 = (EmptyBag A) +* b2;
A2a: support ((EmptyBag A) +* b1) c= (support (EmptyBag A)) \/ (support b1) by Th1;
dom b = (dom b1) \/ (dom b2) by A1, FUNCT_4:def 1;
then dom b1 c= dom b by XBOOLE_1:7;
then B c= dom b by PARTFUN1:def 4;
then A3: B c= A by PARTFUN1:def 4;
dom ((EmptyBag A) +* b1) = (dom (EmptyBag A)) \/ (dom b1) by FUNCT_4:def 1
.= A \/ (dom b1) by PARTFUN1:def 4
.= A \/ B by PARTFUN1:def 4
.= A by A3, XBOOLE_1:12 ;
then reconsider B1 = (EmptyBag A) +* b1 as Rbag of by A2a, PARTFUN1:def 4, POLYNOM1:def 8, RELAT_1:def 18;
A4a: support ((EmptyBag A) +* b2) c= (support (EmptyBag A)) \/ (support b2) by Th1;
dom ((EmptyBag A) +* b2) = (dom (EmptyBag A)) \/ (dom b2) by FUNCT_4:def 1
.= A \/ (dom b2) by PARTFUN1:def 4
.= A \/ (A \ B) by PARTFUN1:def 4
.= A by XBOOLE_1:12 ;
then reconsider B2 = (EmptyBag A) +* b2 as Rbag of by A4a, PARTFUN1:def 4, POLYNOM1:def 8, RELAT_1:def 18;
consider f1 being FinSequence of REAL such that
A5: Sum b1 = Sum f1 and
A6: f1 = b1 * (canFS (support b1)) by UPROOTS:def 3;
consider F1 being FinSequence of REAL such that
A7: Sum B1 = Sum F1 and
A8: F1 = B1 * (canFS (support B1)) by UPROOTS:def 3;
A9: rng (canFS (support b1)) = support b1 by FUNCT_2:def 3;
A10: support b1 c= dom b1 by POLYNOM1:41;
then A11: dom f1 = dom (canFS (support b1)) by A6, A9, RELAT_1:46;
A12: rng (canFS (support B1)) = support B1 by FUNCT_2:def 3;
support B1 c= dom B1 by POLYNOM1:41;
then A13: dom F1 = dom (canFS (support B1)) by A8, A12, RELAT_1:46;

A14: now

let x be set ; :: thesis: ( ( x in support b1 implies x in support B1 ) & ( x in support B1 implies b₁ in support b1 ) )

hereby :: thesis: ( x in support B1 implies b₁ in support b1 )

assume A15: x in support b1 ; :: thesis: x in support B1
then A16: b1 . x <> 0 by POLYNOM1:def 7;
support b1 c= dom b1 by POLYNOM1:41;
then B1 . x = b1 . x by A15, FUNCT_4:14;
hence x in support B1 by A16, POLYNOM1:def 7; :: thesis: verum

end;

assume A17: x in support B1 ; :: thesis: b₁ in support b1
then A18: B1 . x <> 0 by POLYNOM1:def 7;

per cases ( not x in dom b1 or x in dom b1 ) ;

suppose not x in dom b1 ; :: thesis: b₁ in support b1

then B1 . x = (EmptyBag A) . x by FUNCT_4:12
.= 0 by POLYNOM1:56 ;
hence x in support b1 by A17, POLYNOM1:def 7; :: thesis: verum

end;

suppose x in dom b1 ; :: thesis: b₁ in support b1

then B1 . x = b1 . x by FUNCT_4:14;
hence x in support b1 by A18, POLYNOM1:def 7; :: thesis: verum

end;

end;

end;

then A19: support b1 = support B1 by TARSKI:2;
A20: dom f1 = dom F1 by A11, A13, A14, TARSKI:2;

now

let k be Nat; :: thesis: ( k in dom f1 implies f1 . k = F1 . k )
assume A21: k in dom f1 ; :: thesis: f1 . k = F1 . k
A22: (canFS (support b1)) . k in rng (canFS (support b1)) by A11, A21, FUNCT_1:12;
thus f1 . k = b1 . ((canFS (support b1)) . k) by A6, A11, A21, FUNCT_1:23
.= B1 . ((canFS (support b1)) . k) by A9, A10, A22, FUNCT_4:14
.= F1 . k by A8, A11, A19, A21, FUNCT_1:23 ; :: thesis: verum

end;

then A23: Sum B1 = Sum b1 by A5, A7, A20, FINSEQ_1:17;
consider f2 being FinSequence of REAL such that
A24: Sum b2 = Sum f2 and
A25: f2 = b2 * (canFS (support b2)) by UPROOTS:def 3;
consider F2 being FinSequence of REAL such that
A26: Sum B2 = Sum F2 and
A27: F2 = B2 * (canFS (support B2)) by UPROOTS:def 3;
A28: rng (canFS (support b2)) = support b2 by FUNCT_2:def 3;
A29: support b2 c= dom b2 by POLYNOM1:41;
then A30: dom f2 = dom (canFS (support b2)) by A25, A28, RELAT_1:46;
A31: rng (canFS (support B2)) = support B2 by FUNCT_2:def 3;
support B2 c= dom B2 by POLYNOM1:41;
then A32: dom F2 = dom (canFS (support B2)) by A27, A31, RELAT_1:46;

now

let x be set ; :: thesis: ( ( x in support b2 implies x in support B2 ) & ( x in support B2 implies b₁ in support b2 ) )

hereby :: thesis: ( x in support B2 implies b₁ in support b2 )

assume A33: x in support b2 ; :: thesis: x in support B2
then A34: b2 . x <> 0 by POLYNOM1:def 7;
support b2 c= dom b2 by POLYNOM1:41;
then B2 . x = b2 . x by A33, FUNCT_4:14;
hence x in support B2 by A34, POLYNOM1:def 7; :: thesis: verum

end;

assume A35: x in support B2 ; :: thesis: b₁ in support b2
then A36: B2 . x <> 0 by POLYNOM1:def 7;

per cases ( not x in dom b2 or x in dom b2 ) ;

suppose not x in dom b2 ; :: thesis: b₁ in support b2

then B2 . x = (EmptyBag A) . x by FUNCT_4:12
.= 0 by POLYNOM1:56 ;
hence x in support b2 by A35, POLYNOM1:def 7; :: thesis: verum

end;

suppose x in dom b2 ; :: thesis: b₁ in support b2

then B2 . x = b2 . x by FUNCT_4:14;
hence x in support b2 by A36, POLYNOM1:def 7; :: thesis: verum

end;

end;

end;

then A37: support b2 = support B2 by TARSKI:2;

now

let k be Nat; :: thesis: ( k in dom f2 implies f2 . k = F2 . k )
assume A38: k in dom f2 ; :: thesis: f2 . k = F2 . k
A39: (canFS (support b2)) . k in rng (canFS (support b2)) by A30, A38, FUNCT_1:12;
thus f2 . k = b2 . ((canFS (support b2)) . k) by A25, A30, A38, FUNCT_1:23
.= B2 . ((canFS (support b2)) . k) by A28, A29, A39, FUNCT_4:14
.= F2 . k by A27, A30, A37, A38, FUNCT_1:23 ; :: thesis: verum

end;

then A40: Sum B2 = Sum b2 by A24, A26, A32, A37, A25, A28, A29, FINSEQ_1:17, RELAT_1:46;

now

let x be set ; :: thesis: ( x in A implies b . b₁ = (B1 + B2) . b₁ )
assume A41: x in A ; :: thesis: b . b₁ = (B1 + B2) . b₁
A42: dom b1 = B by PARTFUN1:def 4;
A43: dom b2 = A \ B by PARTFUN1:def 4;

per cases ( x in B or not x in B ) ;

suppose A44: x in B ; :: thesis: b . b₁ = (B1 + B2) . b₁

then A45: not x in dom b2 by A43, XBOOLE_0:def 5;
A46: B1 . x = b1 . x by A42, A44, FUNCT_4:14;
B2 . x = (EmptyBag A) . x by A45, FUNCT_4:12
.= 0 by POLYNOM1:56 ;
hence b . x = (B1 . x) + (B2 . x) by A1, A45, A46, FUNCT_4:12
.= (B1 + B2) . x by POLYNOM1:def 5 ;
:: thesis: verum

end;

suppose A47: not x in B ; :: thesis: b . b₁ = (B1 + B2) . b₁

then A48: B1 . x = (EmptyBag A) . x by A42, FUNCT_4:12
.= 0 by POLYNOM1:56 ;
A49: x in dom b2 by A41, A43, A47, XBOOLE_0:def 5;
then B2 . x = b2 . x by FUNCT_4:14;
hence b . x = (B1 . x) + (B2 . x) by A1, A48, A49, FUNCT_4:14
.= (B1 + B2) . x by POLYNOM1:def 5 ;
:: thesis: verum

end;

end;

end;

hence Sum b = (Sum b1) + (Sum b2) by A23, A40, PBOOLE:3, UPROOTS:17; :: thesis: verum