let I be set ; :: thesis: for f, g being Function of I,NAT

for J, K being finite Subset of I

for j being object 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

for j being object st J = {j} holds

Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))

let J, K be finite Subset of I; :: thesis: for j being object st J = {j} holds

Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))

let j be object ; :: thesis: ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )

defpred S_{1}[ Nat] means for I being set

for j being object

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

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

then S_{1}[ card K]
;

hence ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) ) ; :: thesis: verum

for J, K being finite Subset of I

for j being object 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

for j being object st J = {j} holds

Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))

let J, K be finite Subset of I; :: thesis: for j being object st J = {j} holds

Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))

let j be object ; :: thesis: ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )

defpred S

for j being object

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

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 j being object

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 j be object ; :: 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))

end;then A3: ( k = 0 or k >= 1 ) by NAT_1:13;

let I be set ; :: thesis: for j being object

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 j be object ; :: 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;

end;

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

set b = EmptyBag {};

A7: Sum (EmptyBag {}) = 0 by UPROOTS:11;

A8: K = {} by A5, A6;

then ( g | K = {} & [:J,K:] = {} ) ;

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

end;A7: Sum (EmptyBag {}) = 0 by UPROOTS:11;

A8: K = {} by A5, A6;

then ( g | K = {} & [:J,K:] = {} ) ;

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

suppose A9:
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, A9, CARD_1:30;

then consider k9 being object such that

A10: K = {k9} by CARD_1:29;

set b = (multnat * [:f,g:]) | [:J,K:];

consider f9 being FinSequence of REAL such that

A11: Sum ((multnat * [:f,g:]) | [:J,K:]) = Sum f9 and

A12: f9 = ((multnat * [:f,g:]) | [:J,K:]) * (canFS (support ((multnat * [:f,g:]) | [:J,K:]))) by UPROOTS:def 3;

A13: [:J,K:] = {[j,k9]} by A4, A10, ZFMISC_1:29;

then A14: [j,k9] in [:J,K:] by TARSKI:def 1;

then [j,k9] in [:I,I:] ;

then A15: [j,k9] in dom (multnat * [:f,g:]) by FUNCT_2:def 1;

then [:J,K:] c= dom (multnat * [:f,g:]) by A13, ZFMISC_1:31;

then A16: dom ((multnat * [:f,g:]) | [:J,K:]) = [:J,K:] by RELAT_1:62;

Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9)

end;card { the set } = card K by A5, A9, CARD_1:30;

then consider k9 being object such that

A10: K = {k9} by CARD_1:29;

set b = (multnat * [:f,g:]) | [:J,K:];

consider f9 being FinSequence of REAL such that

A11: Sum ((multnat * [:f,g:]) | [:J,K:]) = Sum f9 and

A12: f9 = ((multnat * [:f,g:]) | [:J,K:]) * (canFS (support ((multnat * [:f,g:]) | [:J,K:]))) by UPROOTS:def 3;

A13: [:J,K:] = {[j,k9]} by A4, A10, ZFMISC_1:29;

then A14: [j,k9] in [:J,K:] by TARSKI:def 1;

then [j,k9] in [:I,I:] ;

then A15: [j,k9] in dom (multnat * [:f,g:]) by FUNCT_2:def 1;

then [:J,K:] c= dom (multnat * [:f,g:]) by A13, ZFMISC_1:31;

then A16: dom ((multnat * [:f,g:]) | [:J,K:]) = [:J,K:] by RELAT_1:62;

Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9)

proof

hence
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
by A10, Th27; :: thesis: verum
reconsider I9 = I as non empty set by A4;

reconsider j99 = j, k99 = k9 as Element of I9 by A4, A10, ZFMISC_1:31;

set n1 = f . j;

set n2 = g . k9;

A17: (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 A15, FUNCT_1:12

.= ((multnat * [:f,g:]) | [:J,K:]) . [j,k9] by A14, FUNCT_1:49 ;

end;reconsider j99 = j, k99 = k9 as Element of I9 by A4, A10, ZFMISC_1:31;

set n1 = f . j;

set n2 = g . k9;

A17: (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 A15, FUNCT_1:12

.= ((multnat * [:f,g:]) | [:J,K:]) . [j,k9] by A14, FUNCT_1:49 ;

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

end;

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

then
(f . j) * (g . k9) = 0
by A17, PRE_POLY:def 7;

hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9) by A11, A12, A18, RVSUM_1:72; :: thesis: verum

end;hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k9) by A11, A12, A18, RVSUM_1:72; :: thesis: verum

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 FINSEQ_1:94;

then f9 = <*(((multnat * [:f,g:]) | [:J,K:]) . [j,k9])*> by A12, A14, A16, FINSEQ_2:34;

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

end;then f9 = <*(((multnat * [:f,g:]) | [:J,K:]) . [j,k9])*> by A12, A14, A16, FINSEQ_2:34;

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

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

then
K <> {}
by A5;

then consider k9 being object such that

A20: k9 in K by XBOOLE_0:def 1;

set K0 = {k9};

set K1 = K \ {k9};

reconsider K0 = {k9} as finite Subset of I by A20, ZFMISC_1:31;

card K0 < k by A19, CARD_1:30;

then A21: ( (- 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 A22: [: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 A23: card ((K \ {k9}) \/ K0) = (card (K \ {k9})) + 1 by CARD_2:41;

A24: (K \ {k9}) \/ K0 = K \/ {k9} by XBOOLE_1:39

.= K by A20, 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 A22, Th26

.= ((f . j) * (Sum (g | (K \ {k9})))) + ((f . j) * (Sum (g | K0))) by A2, A4, A5, A23, A24, A21

.= (f . j) * ((Sum (g | (K \ {k9}))) + (Sum (g | K0)))

.= (f . j) * (Sum (g | K)) by A24, Th26, XBOOLE_1:79 ;

:: thesis: verum

end;then consider k9 being object such that

A20: k9 in K by XBOOLE_0:def 1;

set K0 = {k9};

set K1 = K \ {k9};

reconsider K0 = {k9} as finite Subset of I by A20, ZFMISC_1:31;

card K0 < k by A19, CARD_1:30;

then A21: ( (- 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 A22: [: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 A23: card ((K \ {k9}) \/ K0) = (card (K \ {k9})) + 1 by CARD_2:41;

A24: (K \ {k9}) \/ K0 = K \/ {k9} by XBOOLE_1:39

.= K by A20, 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 A22, Th26

.= ((f . j) * (Sum (g | (K \ {k9})))) + ((f . j) * (Sum (g | K0))) by A2, A4, A5, A23, A24, A21

.= (f . j) * ((Sum (g | (K \ {k9}))) + (Sum (g | K0)))

.= (f . j) * (Sum (g | K)) by A24, Th26, XBOOLE_1:79 ;

:: thesis: verum

then S

hence ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) ) ; :: thesis: verum