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

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 A3: k = card J ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K))
( k = 0 or k + 1 > 0 + 1 ) by XREAL_1:10;
then A4: ( k = 0 or k >= 1 ) by NAT_1:13;

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

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

A6: J = {} by A3, A5;
A7: [:J,K:] = {} by A6;
set b = EmptyBag {} ;
A8: EmptyBag {} = {} --> 0 by POLYNOM1:def 15
.= {} ;
Sum (f | J) = 0 by A8, A6, RELAT_1:110, UPROOTS:13;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) by A8, A7, UPROOTS:13, RELAT_1:110; :: thesis: verum

end;

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

consider x being set ;
card {x} = card J by A9, A3, CARD_1:50;
then consider j being set such that
A10: J = {j} by CARD_1:49;
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) by A10, Lm11;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) by A10, Th27; :: thesis: verum

end;

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

then J <> {} by A3;
then consider j being set such that
A12: j in J by XBOOLE_0:def 1;
set J0 = {j};
set J1 = J \ {j};
reconsider J0 = {j} as finite Subset of I by A12, ZFMISC_1:37;
j in J0 by TARSKI:def 1;
then not j in J \ {j} by XBOOLE_0:def 5;
then A13: card ((J \ {j}) \/ J0) = (card (J \ {j})) + 1 by CARD_2:54;
A14: (- 1) + k < 0 + k by XREAL_1:10;
A15: (J \ {j}) \/ J0 = J \/ {j} by XBOOLE_1:39
.= J by A12, ZFMISC_1:46 ;
A16: card J0 < k by A11, CARD_1:50;
A17: [:J,K:] = [:(J \ {j}),K:] \/ [:J0,K:] by A15, ZFMISC_1:120;
A18: J \ {j} misses J0 by XBOOLE_1:79;
A19: Sum (f | J) = (Sum (f | (J \ {j}))) + (Sum (f | J0)) by Th26, A15, XBOOLE_1:79;
A20: [:(J \ {j}),K:] misses [:J0,K:] by A18, ZFMISC_1:127;
A21: Sum ((multnat * [:f,g:]) | [:J0,K:]) = (Sum (f | J0)) * (Sum (g | K)) by A16, A2;
thus Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum ((multnat * [:f,g:]) | [:(J \ {j}),K:])) + (Sum ((multnat * [:f,g:]) | [:J0,K:])) by A20, Th26, A17
.= ((Sum (f | (J \ {j}))) * (Sum (g | K))) + ((Sum (f | J0)) * (Sum (g | K))) by A21, A2, A14, A3, A13, A15
.= (Sum (f | J)) * (Sum (g | K)) by A19 ; :: thesis: verum

end;

end;

end;

end;

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