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 S1[ 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
S1[n] ) holds
S1[k]
proof
let k be Nat; :: thesis: ( ( 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] ; :: thesis: S1[k]
thus S1[k] :: thesis: verum
proof
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 A3: J = {j} ; :: thesis: ( not k = card K or Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) )
assume A4: k = card K ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
( k = 0 or k + 1 > 0 + 1 ) by XREAL_1:10;
then A5: ( k = 0 or k >= 1 ) by NAT_1:13;
per cases ( k = 0 or k = 1 or k > 1 ) by A5, XXREAL_0:1;
suppose A6: k = 0 ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
A7: K = {} by A4, A6;
A8: g | K = {} by A7;
A9: [:J,K:] = {} by A7;
set b = EmptyBag {} ;
A10: EmptyBag {} = {} --> 0 by POLYNOM1:def 15
.= {} ;
Sum (EmptyBag {} ) = 0 by UPROOTS:13;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) by A7, A8, A10, A9; :: thesis: verum
end;
suppose A11: k = 1 ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
consider x being set ;
card {x} = card K by A11, A4, CARD_1:50;
then consider k' being set such that
A12: K = {k'} by CARD_1:49;
set b = (multnat * [:f,g:]) | [:J,K:];
consider f' being FinSequence of REAL such that
A13: ( Sum ((multnat * [:f,g:]) | [:J,K:]) = Sum f' & f' = ((multnat * [:f,g:]) | [:J,K:]) * (canFS (support ((multnat * [:f,g:]) | [:J,K:]))) ) by UPROOTS:def 3;
A14: [:J,K:] = {[j,k']} by ZFMISC_1:35, A12, A3;
then A15: [j,k'] in [:J,K:] by TARSKI:def 1;
then [j,k'] in [:I,I:] ;
then A16: [j,k'] in dom (multnat * [:f,g:]) by FUNCT_2:def 1;
then [:J,K:] c= dom (multnat * [:f,g:]) by A14, ZFMISC_1:37;
then A17: dom ((multnat * [:f,g:]) | [:J,K:]) = [:J,K:] by RELAT_1:91;
then A18: support ((multnat * [:f,g:]) | [:J,K:]) c= [:J,K:] by POLYNOM1:41;
Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k')
proof
set n1 = f . j;
set n2 = g . k';
reconsider I' = I as non empty set by A3;
reconsider j'' = j, k'' = k' as Element of I' by A3, A12, ZFMISC_1:37;
A19: (f . j) * (g . k') = multnat . (f . j),(g . k') by BINOP_2:def 24
.= multnat . [(f . j''),(g . k'')] by BINOP_1:def 1
.= multnat . ([:f,g:] . j'',k'') by FUNCT_3:96
.= multnat . ([:f,g:] . [j,k']) by BINOP_1:def 1
.= (multnat * [:f,g:]) . [j,k'] by A16, FUNCT_1:22
.= ((multnat * [:f,g:]) | [:J,K:]) . [j,k'] by A15, FUNCT_1:72 ;
per cases ( support ((multnat * [:f,g:]) | [:J,K:]) = {} or support ((multnat * [:f,g:]) | [:J,K:]) = {[j,k']} ) by A14, A18, ZFMISC_1:39;
suppose A20: support ((multnat * [:f,g:]) | [:J,K:]) = {} ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k')
(f . j) * (g . k') = 0 by A19, A20, POLYNOM1:def 7;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k') by A20, A13, RVSUM_1:102; :: thesis: verum
end;
suppose support ((multnat * [:f,g:]) | [:J,K:]) = {[j,k']} ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k')
then A21: canFS (support ((multnat * [:f,g:]) | [:J,K:])) = <*[j,k']*> by UPROOTS:6;
f' = <*(((multnat * [:f,g:]) | [:J,K:]) . [j,k'])*> by A15, A17, A21, A13, BAGORDER:3;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (g . k') by A19, A13, RVSUM_1:103; :: thesis: verum
end;
end;
end;
hence Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) by A12, Th27; :: thesis: verum
end;
suppose A22: k > 1 ; :: thesis: Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K))
then K <> {} by A4;
then consider k' being set such that
A23: k' in K by XBOOLE_0:def 1;
set K0 = {k'};
set K1 = K \ {k'};
reconsider K0 = {k'} as finite Subset of I by A23, ZFMISC_1:37;
k' in K0 by TARSKI:def 1;
then not k' in K \ {k'} by XBOOLE_0:def 5;
then A24: card ((K \ {k'}) \/ K0) = (card (K \ {k'})) + 1 by CARD_2:54;
A25: (- 1) + k < 0 + k by XREAL_1:10;
A26: (K \ {k'}) \/ K0 = K \/ {k'} by XBOOLE_1:39
.= K by A23, ZFMISC_1:46 ;
A27: card K0 < k by A22, CARD_1:50;
A28: [:J,K:] = [:J,(K \ {k'}):] \/ [:J,K0:] by A26, ZFMISC_1:120;
A29: K \ {k'} misses K0 by XBOOLE_1:79;
A30: [:J,(K \ {k'}):] misses [:J,K0:] by A29, ZFMISC_1:127;
A31: Sum ((multnat * [:f,g:]) | [:J,K0:]) = (f . j) * (Sum (g | K0)) by A27, A3, A2;
thus Sum ((multnat * [:f,g:]) | [:J,K:]) = (Sum ((multnat * [:f,g:]) | [:J,(K \ {k'}):])) + (Sum ((multnat * [:f,g:]) | [:J,K0:])) by A30, Th26, A28
.= ((f . j) * (Sum (g | (K \ {k'})))) + ((f . j) * (Sum (g | K0))) by A26, A3, A2, A31, A25, A4, A24
.= (f . j) * ((Sum (g | (K \ {k'}))) + (Sum (g | K0)))
.= (f . j) * (Sum (g | K)) by Th26, A26, XBOOLE_1:79 ; :: thesis: verum
end;
end;
end;
end;
A32: for k being Nat holds S1[k] from NAT_1:sch 4(A1);
 S1[ card K] by A32;
hence ( J = {j} implies Sum ((multnat * [:f,g:]) | [:J,K:]) = (f . j) * (Sum (g | K)) ) ; :: thesis: verum