let I be set ; :: thesis: for p, q being Bags I -valued FinSequence holds Sum (p ^ q) = (Sum p) + (Sum q)
let p, q be Bags I -valued FinSequence; :: thesis: Sum (p ^ q) = (Sum p) + (Sum q)
set f = p ^ q;
consider F being Function of NAT,(Bags I) such that
A1: Sum (p ^ q) = F . (len (p ^ q)) and
A2: F . 0 = EmptyBag I and
A3: for i being Nat
for b being bag of I st i < len (p ^ q) & b = (p ^ q) . (i + 1) holds
F . (i + 1) = (F . i) + b by SUM;
consider F1 being Function of NAT,(Bags I) such that
A4: Sum p = F1 . (len p) and
A5: F1 . 0 = EmptyBag I and
A6: for i being Nat
for b being bag of I st i < len p & b = p . (i + 1) holds
F1 . (i + 1) = (F1 . i) + b by SUM;
consider F2 being Function of NAT,(Bags I) such that
B1: Sum q = F2 . (len q) and
B2: F2 . 0 = EmptyBag I and
B3: for i being Nat
for b being bag of I st i < len q & b = q . (i + 1) holds
F2 . (i + 1) = (F2 . i) + b by SUM;
defpred S₁[ Nat] means ( $1 <= len p implies F . $1 = F1 . $1 );
A7: S₁[ 0 ] by A2, A5;
A8: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A9: ( S₁[i] & i + 1 <= len p ) ; :: thesis: F . (i + 1) = F1 . (i + 1)
then ( i < len p & len p <= (len p) + (len q) & (len p) + (len q) = len (p ^ q) ) by FINSEQ_1:22, NAT_1:11, NAT_1:13;
then A11: i < len (p ^ q) by XXREAL_0:2;
A12: i + 1 in dom p by A9, NAT_1:11, FINSEQ_3:25;
then reconsider b = p . (i + 1) as Element of Bags I by FUNCT_1:102;
(p ^ q) . (i + 1) = b by A12, FINSEQ_1:def 7;
hence F . (i + 1) = (F . i) + b by A3, A11
.= (F1 . i) + b by A9, NAT_1:13
.= F1 . (i + 1) by A6, A9, NAT_1:13 ;
:: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A7, A8);
then A13: Sum p = F . (len p) by A4;
defpred S₂[ Nat] means ( $1 <= len q implies F . ((len p) + $1) = (Sum p) + (F2 . $1) );
A14: S₂[ 0 ] by A13, B2, PRE_POLY:53;
A15: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A9: ( S₂[i] & i + 1 <= len q ) ; :: thesis: F . ((len p) + (i + 1)) = (Sum p) + (F2 . (i + 1))
then A10: ( i < len q & (len p) + (len q) = len (p ^ q) ) by FINSEQ_1:22, NAT_1:13;
A12: i + 1 in dom q by A9, NAT_1:11, FINSEQ_3:25;
then reconsider b = q . (i + 1) as Element of Bags I by FUNCT_1:102;
reconsider lp = len p as Nat ;
reconsider lpi = lp + i as Nat ;
( (p ^ q) . ((len p) + (i + 1)) = b & (len p) + (i + 1) = ((len p) + i) + 1 ) by A12, FINSEQ_1:def 7;
hence F . ((len p) + (i + 1)) = (F . lpi) + b by A3, A10, XREAL_1:6
.= ((Sum p) + (F2 . i)) + b by A9, NAT_1:13
.= (Sum p) + ((F2 . i) + b) by RFUNCT_1:8
.= (Sum p) + (F2 . (i + 1)) by B3, A9, NAT_1:13 ;
:: thesis: verum

end;

for i being Nat holds S₂[i] from NAT_1:sch 2(A14, A15);
then F . ((len p) + (len q)) = (Sum p) + (Sum q) by B1;
hence Sum (p ^ q) = (Sum p) + (Sum q) by A1, FINSEQ_1:22; :: thesis: verum