let I be set ; :: thesis: for f, g being Function of I,NAT
for J, K being finite Subset of I holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))
let f, g be Function of I,NAT; :: thesis: for J, K being finite Subset of I holds Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))
let J, K be finite Subset of I; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))
defpred S₁[ Nat] means for I being set
for f, g being Function of I,NAT
for J, K being finite Subset of I st $1 = card J holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K));
A1: for k being Nat st ( for n being Nat st n < k holds
S₁[n] ) holds
S₁[k]

proof

let k be Nat; :: thesis: ( ( for n being Nat st n < k holds
S₁[n] ) implies S₁[k] )
assume A2: for n being Nat st n < k holds
S₁[n] ; :: thesis: S₁[k]
thus S₁[k] :: thesis: verum

proof

( k = 0 or k + 1 > 0 + 1 ) by XREAL_1:8;
then A3: ( k = 0 or k >= 1 ) by NAT_1:13;
let I be set ; :: thesis: for f, g being Function of I,NAT
for J, K being finite Subset of I st k = card J holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))
let f, g be Function of I,NAT; :: thesis: for J, K being finite Subset of I st k = card J holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))
let J, K be finite Subset of I; :: thesis: ( k = card J implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) )
assume A4: k = card J ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))

per cases ( k = 0 or k = 1 or k > 1 ) by A3, XXREAL_0:1;

suppose k = 0 ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))

then A5: J = {} by A4;
then A6: [:J,K:] = {} ;
A7: EmptyBag {} = {} --> 0
.= {} ;
then Sum (f | J) = 0 by A5, RELAT_1:81, UPROOTS:11;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) by A6, A7, RELAT_1:81, UPROOTS:11; :: thesis: verum

end;

suppose A8: k = 1 ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))

set x = the set ;
card { the set } = card J by A4, A8, CARD_1:30;
then consider j being object such that
A9: J = {j} by CARD_1:29;
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) by A9, Lm11;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) by A9, Th27; :: thesis: verum

end;

suppose A10: k > 1 ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))

then J <> {} by A4;
then consider j being object such that
A11: j in J by XBOOLE_0:def 1;
set J0 = {j};
set J1 = J \ {j};
reconsider J0 = {j} as finite Subset of I by A11, ZFMISC_1:31;
A12: (J \ {j}) \/ J0 = J \/ {j} by XBOOLE_1:39
.= J by A11, ZFMISC_1:40 ;
then A13: Sum (f | J) = (Sum (f | (J \ {j}))) + (Sum (f | J0)) by Th26, XBOOLE_1:79;
card J0 < k by A10, CARD_1:30;
then A14: ( (- 1) + k < 0 + k & Sum ((multnat * [:f,g:]) | [:J0,K:]) = (Sum (f | J0)) * (Sum (g | K)) ) by A2, XREAL_1:8;
J \ {j} misses J0 by XBOOLE_1:79;
then A15: [:(J \ {j}),K:] misses [:J0,K:] by ZFMISC_1:104;
j in J0 by TARSKI:def 1;
then not j in J \ {j} by XBOOLE_0:def 5;
then A16: card ((J \ {j}) \/ J0) = (card (J \ {j})) + 1 by CARD_2:41;
[:J,K:] = [:(J \ {j}),K:] \/ [:J0,K:] by A12, ZFMISC_1:97;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum ((multnat * [:f,g:]) | [:(J \ {j}),K:])) + (Sum ((multnat * [:f,g:]) | [:J0,K:])) by A15, Th26
.= ((Sum (f | (J \ {j}))) * (Sum (g | K))) + ((Sum (f | J0)) * (Sum (g | K))) by A2, A4, A16, A12, A14
.= (Sum (f | J)) * (Sum (g | K)) by A13 ;
:: thesis: verum

end;

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 4(A1);
then S₁[ card J] ;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) ; :: thesis: verum