let F, G be sequence of ExtREAL; :: thesis: ( G is nonnegative implies for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G )
assume A1: G is nonnegative ; :: thesis: for S being non empty Subset of NAT
for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G
let S be non empty Subset of NAT; :: thesis: for H being Function of S,NAT st H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) holds
SUM F <= SUM G
let H be Function of S,NAT; :: thesis: ( H is one-to-one & ( for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ) implies SUM F <= SUM G )
assume A2: H is one-to-one ; :: thesis: ( ex k being Element of NAT st
( ( k in S implies F . k = (G * H) . k ) implies ( not k in S & not F . k = 0. ) ) or SUM F <= SUM G )
assume for k being Element of NAT holds
( ( k in S implies F . k = (G * H) . k ) & ( not k in S implies F . k = 0. ) ) ; :: thesis: SUM F <= SUM G
then F = On (G * H) by Def1;
hence SUM F <= SUM G by A1, A2, Th10; :: thesis: verum