let I, j be set ; :: thesis: for f, g being Function of I,NAT
for J, K being finite Subset of I st J = {j} holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
let f, g be Function of I,NAT; :: thesis: for J, K being finite Subset of I st J = {j} holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
let J, K be finite Subset of I; :: thesis: ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )
defpred S₁[ Nat] means for I, j being set
for f, g being Function of I,NAT
for J, K being finite Subset of I st J = {j} & $1 = card K holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (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, j be set ; :: thesis: for f, g being Function of I,NAT
for J, K being finite Subset of I st J = {j} & k = card K holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
let f, g be Function of I,NAT; :: thesis: for J, K being finite Subset of I st J = {j} & k = card K holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
let J, K be finite Subset of I; :: thesis: ( J = {j} & k = card K implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )
assume A4: J = {j} ; :: thesis: ( not k = card K or Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )
assume A5: k = card K ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))

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

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

set b = EmptyBag {};
A7: EmptyBag {} = {} --> 0 by PRE_POLY:def 13
.= {} ;
A8: Sum (EmptyBag {}) = 0 by UPROOTS:11;
A9: K = {} by A5, A6;
then ( g | K = {} & [:J,K:] = {} ) ;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) by A9, A7, A8; :: thesis: verum

end;

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

set x = the set ;
card { the set } = card K by A5, A10, CARD_1:30;
then consider k9 being set such that
A11: K = {k9} by CARD_1:29;
set b = (multnat * [:f,g:]) | [:J,K:];
consider f9 being FinSequence of REAL such that
A12: Sum ((multnat * [:f,g:]) | [:J,K:]) = Sum f9 and
A13: f9 = ((multnat * [:f,g:]) | [:J,K:]) * (canFS (support ((multnat * [:f,g:]) | [:J,K:]))) by UPROOTS:def 3;
A14: [:J,K:] = {[j,k9]} by A4, A11, ZFMISC_1:29;
then A15: [j,k9] in [:J,K:] by TARSKI:def 1;
then [j,k9] in [:I,I:] ;
then A16: [j,k9] in dom (multnat * [:f,g:]) by FUNCT_2:def 1;
then [:J,K:] c= dom (multnat * [:f,g:]) by A14, ZFMISC_1:31;
then A17: dom ((multnat * [:f,g:]) | [:J,K:]) = [:J,K:] by RELAT_1:62;
then A18: support ((multnat * [:f,g:]) | [:J,K:]) c= [:J,K:] by PRE_POLY:37;
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9)

proof

reconsider I9 = I as non empty set by A4;
reconsider j99 = j, k99 = k9 as Element of I9 by A4, A11, ZFMISC_1:31;
set n1 = f . j;
set n2 = g . k9;
A19: (f . j) * (g . k9) = multnat . ((f . j),(g . k9)) by BINOP_2:def 24
.= multnat . [(f . j99),(g . k99)] by BINOP_1:def 1
.= multnat . ([:f,g:] . (j99,k99)) by FUNCT_3:75
.= multnat . ([:f,g:] . [j,k9]) by BINOP_1:def 1
.= (multnat * [:f,g:]) . [j,k9] by A16, FUNCT_1:12
.= ((multnat * [:f,g:]) | [:J,K:]) . [j,k9] by A15, FUNCT_1:49 ;

per cases ( support ((multnat * [:f,g:]) | [:J,K:]) = {} or support ((multnat * [:f,g:]) | [:J,K:]) = {[j,k9]} ) by A14, A18, ZFMISC_1:33;

suppose A20: support ((multnat * [:f,g:]) | [:J,K:]) = {} ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9)

then (f . j) * (g . k9) = 0 by A19, PRE_POLY:def 7;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9) by A12, A13, A20, RVSUM_1:72; :: thesis: verum

end;

suppose support ((multnat * [:f,g:]) | [:J,K:]) = {[j,k9]} ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9)

then canFS (support ((multnat * [:f,g:]) | [:J,K:])) = <*[j,k9]*> by UPROOTS:4;
then f9 = <*(((multnat * [:f,g:]) | [:J,K:]) . [j,k9])*> by A13, A15, A17, FINSEQ_2:34;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9) by A12, A19, RVSUM_1:73; :: thesis: verum

end;

end;

end;

hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) by A11, Th27; :: thesis: verum

end;

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

then K <> {} by A5;
then consider k9 being set such that
A22: k9 in K by XBOOLE_0:def 1;
set K0 = {k9};
set K1 = K \ {k9};
reconsider K0 = {k9} as finite Subset of I by A22, ZFMISC_1:31;
card K0 < k by A21, CARD_1:30;
then A23: ( (- 1) + k < 0 + k & Sum ((multnat * [:f,g:]) | [:J,K0:]) = (f . j) * (Sum (g | K0)) ) by A2, A4, XREAL_1:8;
K \ {k9} misses K0 by XBOOLE_1:79;
then A24: [:J,(K \ {k9}):] misses [:J,K0:] by ZFMISC_1:104;
k9 in K0 by TARSKI:def 1;
then not k9 in K \ {k9} by XBOOLE_0:def 5;
then A25: card ((K \ {k9}) \/ K0) = (card (K \ {k9})) + 1 by CARD_2:41;
A26: (K \ {k9}) \/ K0 = K \/ {k9} by XBOOLE_1:39
.= K by A22, ZFMISC_1:40 ;
then [:J,K:] = [:J,(K \ {k9}):] \/ [:J,K0:] by ZFMISC_1:97;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum ((multnat * [:f,g:]) | [:J,(K \ {k9}):])) + (Sum ((multnat * [:f,g:]) | [:J,K0:])) by A24, Th26
.= ((f . j) * (Sum (g | (K \ {k9})))) + ((f . j) * (Sum (g | K0))) by A2, A4, A5, A25, A26, A23
.= (f . j) * ((Sum (g | (K \ {k9}))) + (Sum (g | K0)))
.= (f . j) * (Sum (g | K)) by A26, Th26, XBOOLE_1:79 ;
:: thesis: verum

end;

end;

end;

end;

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