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_{1}[ 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_{1}[n] ) holds

S_{1}[k]
_{1}[k]
from NAT_1:sch 4(A1);

then S_{1}[ card J]
;

hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) ; :: thesis: verum

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

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

S

proof

for k being Nat holds S
let k be Nat; :: thesis: ( ( for n being Nat st n < k holds

S_{1}[n] ) implies S_{1}[k] )

assume A2: for n being Nat st n < k holds

S_{1}[n]
; :: thesis: S_{1}[k]

thus S_{1}[k]
:: thesis: verum

end;S

assume A2: for n being Nat st n < k holds

S

thus S

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))

end;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;

end;

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;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

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;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

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;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

then S

hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum (f | J)) * (Sum (g | K)) ; :: thesis: verum