let I be set ; 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; 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; for j being object st J = {j} holds
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
let j be object ; ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )
defpred S1[ 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
S1[n] ) holds
S1[k]
proof
let k be
Nat;
( ( for n being Nat st n < k holds
S1[n] ) implies S1[k] )
assume A2:
for
n being
Nat st
n < k holds
S1[
n]
;
S1[k]
thus
S1[
k]
verumproof
(
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 ;
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 ;
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;
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;
( J = {j} & k = card K implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )
assume A4:
J = {j}
;
( not k = card K or Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )
assume A5:
k = card K
;
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 A9:
k = 1
;
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)
proof
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
;
per cases
( support ((multnat * [:f,g:]) | [:J,K:]) = {} or support ((multnat * [:f,g:]) | [:J,K:]) = {[j,k9]} )
by A13, ZFMISC_1:33;
suppose
support ((multnat * [:f,g:]) | [:J,K:]) = {[j,k9]}
;
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;
verum end; end;
end; hence
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
by A10, Th27;
verum end; suppose A19:
k > 1
;
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
;
verum end; end;
end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 4(A1);
then
S1[ card K]
;
hence
( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )
; verum