let A, B be set ; :: thesis: for b being Rbag of A
for b1 being Rbag of B
for b2 being Rbag of A \ B st b = b1 +* b2 holds
Sum b = (Sum b1) + (Sum b2)
let b be Rbag of A; :: thesis: for b1 being Rbag of B
for b2 being Rbag of A \ B st b = b1 +* b2 holds
Sum b = (Sum b1) + (Sum b2)
let b1 be Rbag of B; :: thesis: for b2 being Rbag of A \ B st b = b1 +* b2 holds
Sum b = (Sum b1) + (Sum b2)
let b2 be Rbag of A \ B; :: thesis: ( b = b1 +* b2 implies Sum b = (Sum b1) + (Sum b2) )
assume A1: b = b1 +* b2 ; :: thesis: Sum b = (Sum b1) + (Sum b2)
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 2;
then A2: B c= A by PARTFUN1:def 2;
set B1 = (EmptyBag A) +* b1;
A3: dom ((EmptyBag A) +* b1) = (dom (EmptyBag A)) \/ (dom b1) by FUNCT_4:def 1
.= A \/ (dom b1) by PARTFUN1:def 2
.= A \/ B by PARTFUN1:def 2
.= A by A2, XBOOLE_1:12 ;
support ((EmptyBag A) +* b1) c= (support (EmptyBag A)) \/ (support b1) by Th1;
then reconsider B1 = (EmptyBag A) +* b1 as Rbag of A by A3, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;
set B2 = (EmptyBag A) +* b2;
A4: dom ((EmptyBag A) +* b2) = (dom (EmptyBag A)) \/ (dom b2) by FUNCT_4:def 1
.= A \/ (dom b2) by PARTFUN1:def 2
.= A \/ (A \ B) by PARTFUN1:def 2
.= A by XBOOLE_1:12 ;
support ((EmptyBag A) +* b2) c= (support (EmptyBag A)) \/ (support b2) by Th1;
then reconsider B2 = (EmptyBag A) +* b2 as Rbag of A by A4, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

A5: now :: thesis: for x being object st x in A holds
b . x = (B1 + B2) . x

let x be object ; :: thesis: ( x in A implies b . b₁ = (B1 + B2) . b₁ )
assume A6: x in A ; :: thesis: b . b₁ = (B1 + B2) . b₁
A7: dom b1 = B by PARTFUN1:def 2;
A8: dom b2 = A \ B by PARTFUN1:def 2;

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

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

then A10: B1 . x = b1 . x by A7, FUNCT_4:13;
A11: not x in dom b2 by A9, XBOOLE_0:def 5;
then B2 . x = (EmptyBag A) . x by FUNCT_4:11
.= 0 by PBOOLE:5 ;
hence b . x = (B1 . x) + (B2 . x) by A1, A11, A10, FUNCT_4:11
.= (B1 + B2) . x by PRE_POLY:def 5 ;
:: thesis: verum

end;

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

then A13: B1 . x = (EmptyBag A) . x by A7, FUNCT_4:11
.= 0 by PBOOLE:5 ;
A14: x in dom b2 by A6, A8, A12, XBOOLE_0:def 5;
then B2 . x = b2 . x by FUNCT_4:13;
hence b . x = (B1 . x) + (B2 . x) by A1, A13, A14, FUNCT_4:13
.= (B1 + B2) . x by PRE_POLY:def 5 ;
:: thesis: verum

end;

end;

end;

consider F2 being FinSequence of REAL such that
A15: Sum B2 = Sum F2 and
A16: F2 = B2 * (canFS (support B2)) by UPROOTS:def 3;
( rng (canFS (support B2)) = support B2 & support B2 c= dom B2 ) by FUNCT_2:def 3, PRE_POLY:37;
then A17: dom F2 = dom (canFS (support B2)) by A16, RELAT_1:27;
consider F1 being FinSequence of REAL such that
A18: Sum B1 = Sum F1 and
A19: F1 = B1 * (canFS (support B1)) by UPROOTS:def 3;
consider f1 being FinSequence of REAL such that
A20: Sum b1 = Sum f1 and
A21: f1 = b1 * (canFS (support b1)) by UPROOTS:def 3;
A22: ( rng (canFS (support b1)) = support b1 & support b1 c= dom b1 ) by FUNCT_2:def 3, PRE_POLY:37;
then A23: dom f1 = dom (canFS (support b1)) by A21, RELAT_1:27;

A24: now :: thesis: for x being object holds
( ( x in support b1 implies x in support B1 ) & ( x in support B1 implies x in support b1 ) )

let x be object ; :: 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 A25: x in support b1 ; :: thesis: x in support B1
then A26: b1 . x <> 0 by PRE_POLY:def 7;
support b1 c= dom b1 by PRE_POLY:37;
then B1 . x = b1 . x by A25, FUNCT_4:13;
hence x in support B1 by A26, PRE_POLY:def 7; :: thesis: verum

end;

assume A27: x in support B1 ; :: thesis: b₁ in support b1
then A28: B1 . x <> 0 by PRE_POLY: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:11
.= 0 by PBOOLE:5 ;
hence x in support b1 by A27, PRE_POLY:def 7; :: thesis: verum

end;

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

then B1 . x = b1 . x by FUNCT_4:13;
hence x in support b1 by A28, PRE_POLY:def 7; :: thesis: verum

end;

end;

end;

then A29: support b1 = support B1 by TARSKI:2;

A30: now :: thesis: for k being Nat st k in dom f1 holds
f1 . k = F1 . k

let k be Nat; :: thesis: ( k in dom f1 implies f1 . k = F1 . k )
assume A31: k in dom f1 ; :: thesis: f1 . k = F1 . k
A32: (canFS (support b1)) . k in rng (canFS (support b1)) by A23, A31, FUNCT_1:3;
thus f1 . k = b1 . ((canFS (support b1)) . k) by A21, A23, A31, FUNCT_1:13
.= B1 . ((canFS (support b1)) . k) by A22, A32, FUNCT_4:13
.= F1 . k by A19, A23, A29, A31, FUNCT_1:13 ; :: thesis: verum

end;

( rng (canFS (support B1)) = support B1 & support B1 c= dom B1 ) by FUNCT_2:def 3, PRE_POLY:37;
then dom F1 = dom (canFS (support B1)) by A19, RELAT_1:27;
then dom f1 = dom F1 by A23, A24, TARSKI:2;
then A33: Sum B1 = Sum b1 by A20, A18, A30, FINSEQ_1:13;
consider f2 being FinSequence of REAL such that
A34: Sum b2 = Sum f2 and
A35: f2 = b2 * (canFS (support b2)) by UPROOTS:def 3;
A36: ( rng (canFS (support b2)) = support b2 & support b2 c= dom b2 ) by FUNCT_2:def 3, PRE_POLY:37;
then A37: dom f2 = dom (canFS (support b2)) by A35, RELAT_1:27;

now :: thesis: for x being object holds
( ( x in support b2 implies x in support B2 ) & ( x in support B2 implies x in support b2 ) )

let x be object ; :: 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 A38: x in support b2 ; :: thesis: x in support B2
then A39: b2 . x <> 0 by PRE_POLY:def 7;
support b2 c= dom b2 by PRE_POLY:37;
then B2 . x = b2 . x by A38, FUNCT_4:13;
hence x in support B2 by A39, PRE_POLY:def 7; :: thesis: verum

end;

assume A40: x in support B2 ; :: thesis: b₁ in support b2
then A41: B2 . x <> 0 by PRE_POLY: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:11
.= 0 by PBOOLE:5 ;
hence x in support b2 by A40, PRE_POLY:def 7; :: thesis: verum

end;

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

then B2 . x = b2 . x by FUNCT_4:13;
hence x in support b2 by A41, PRE_POLY:def 7; :: thesis: verum

end;

end;

end;

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

now :: thesis: for k being Nat st k in dom f2 holds
f2 . k = F2 . k

let k be Nat; :: thesis: ( k in dom f2 implies f2 . k = F2 . k )
assume A43: k in dom f2 ; :: thesis: f2 . k = F2 . k
A44: (canFS (support b2)) . k in rng (canFS (support b2)) by A37, A43, FUNCT_1:3;
thus f2 . k = b2 . ((canFS (support b2)) . k) by A35, A37, A43, FUNCT_1:13
.= B2 . ((canFS (support b2)) . k) by A36, A44, FUNCT_4:13
.= F2 . k by A16, A37, A42, A43, FUNCT_1:13 ; :: thesis: verum

end;

then Sum B2 = Sum b2 by A34, A35, A15, A36, A17, A42, FINSEQ_1:13, RELAT_1:27;
hence Sum b = (Sum b1) + (Sum b2) by A33, A5, PBOOLE:3, UPROOTS:15; :: thesis: verum