let G be Function of NAT ,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 holds
SUM (On (G * H)) <= 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 holds
SUM (On (G * H)) <= SUM G
let S be non empty Subset of NAT ; :: thesis: for H being Function of S,NAT st H is one-to-one holds
SUM (On (G * H)) <= SUM G
let H be Function of S,NAT ; :: thesis: ( H is one-to-one implies SUM (On (G * H)) <= SUM G )
assume A2: H is one-to-one ; :: thesis: SUM (On (G * H)) <= SUM G
defpred S1[ Element of NAT ] means ex m being Element of NAT st
for F being Function of NAT ,ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . $1 <= (Ser F) . m;
A3: S1[ 0 ]
proof
per cases ( 0 in S or not 0 in S ) ;
suppose A4: 0 in S ; :: thesis: S1[ 0 ]
reconsider m = H . 0 as Element of NAT ;
take m ; :: thesis: for F being Function of NAT ,ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . 0 <= (Ser F) . m
let F be Function of NAT ,ExtREAL ; :: thesis: ( F is nonnegative implies (Ser (On (F * H))) . 0 <= (Ser F) . m )
assume A5: F is nonnegative ; :: thesis: (Ser (On (F * H))) . 0 <= (Ser F) . m
(Ser (On (F * H))) . 0 = (On (F * H)) . 0 by SUPINF_2:63;
then (Ser (On (F * H))) . 0 = (F * H) . 0 by A4, Def1
.= F . (H . 0 ) by A4, FUNCT_2:21 ;
hence (Ser (On (F * H))) . 0 <= (Ser F) . m by A5, Th2; :: thesis: verum
end;
suppose A6: not 0 in S ; :: thesis: S1[ 0 ]
take m = 0 ; :: thesis: for F being Function of NAT ,ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . 0 <= (Ser F) . m
let F be Function of NAT ,ExtREAL ; :: thesis: ( F is nonnegative implies (Ser (On (F * H))) . 0 <= (Ser F) . m )
assume A7: F is nonnegative ; :: thesis: (Ser (On (F * H))) . 0 <= (Ser F) . m
(Ser (On (F * H))) . 0 = (On (F * H)) . 0 by SUPINF_2:63;
then A8: (Ser (On (F * H))) . 0 = 0. by A6, Def1;
A9: 0. <= F . 0 by A7, SUPINF_2:58;
F . 0 <= (Ser F) . m by A7, Th2;
hence (Ser (On (F * H))) . 0 <= (Ser F) . m by A8, A9, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A10: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
given m0 being Element of NAT such that A11: for F being Function of NAT ,ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . k <= (Ser F) . m0 ; :: thesis: S1[k + 1]
per cases ( k + 1 in S or not k + 1 in S ) ;
suppose A12: k + 1 in S ; :: thesis: S1[k + 1]
reconsider m1 = H . (k + 1) as Element of NAT ;
set m = m0 + m1;
A13: m1 <= m0 + m1 by NAT_1:11;
take m0 + m1 ; :: thesis: for F being Function of NAT ,ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1)
let F be Function of NAT ,ExtREAL ; :: thesis: ( F is nonnegative implies (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) )
assume A14: F is nonnegative ; :: thesis: (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1)
defpred S2[ Element of NAT , Element of ExtREAL ] means ( ( $1 = H . (k + 1) implies $2 = F . $1 ) & ( $1 <> H . (k + 1) implies $2 = 0. ) );
A15: for n being Element of NAT ex y being Element of ExtREAL st S2[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of ExtREAL st S2[n,y]
per cases ( n = H . (k + 1) or n <> H . (k + 1) ) ;
suppose A16: n = H . (k + 1) ; :: thesis: ex y being Element of ExtREAL st S2[n,y]
take F . n ; :: thesis: S2[n,F . n]
thus S2[n,F . n] by A16; :: thesis: verum
end;
suppose A17: n <> H . (k + 1) ; :: thesis: ex y being Element of ExtREAL st S2[n,y]
take 0. ; :: thesis: S2[n, 0. ]
thus S2[n, 0. ] by A17; :: thesis: verum
end;
end;
end;
consider G0 being Function of NAT ,ExtREAL such that
A18: for n being Element of NAT holds S2[n,G0 . n] from FUNCT_2:sch 3(A15);
 for n being Element of NAT holds 0. <= G0 . n
proof
let n be Element of NAT ; :: thesis: 0. <= G0 . n
per cases ( n = H . (k + 1) or not n = H . (k + 1) ) ;
suppose n = H . (k + 1) ; :: thesis: 0. <= G0 . n
then G0 . n = F . n by A18;
hence 0. <= G0 . n by A14, SUPINF_2:58; :: thesis: verum
end;
suppose not n = H . (k + 1) ; :: thesis: 0. <= G0 . n
hence 0. <= G0 . n by A18; :: thesis: verum
end;
end;
end;
then A19: G0 is nonnegative by SUPINF_2:58;
defpred S3[ Element of NAT , Element of ExtREAL ] means ( ( $1 <> H . (k + 1) implies $2 = F . $1 ) & ( $1 = H . (k + 1) implies $2 = 0. ) );
A20: for n being Element of NAT ex y being Element of ExtREAL st S3[n,y]
proof
let n be Element of NAT ; :: thesis: ex y being Element of ExtREAL st S3[n,y]
per cases ( n <> H . (k + 1) or n = H . (k + 1) ) ;
suppose A21: n <> H . (k + 1) ; :: thesis: ex y being Element of ExtREAL st S3[n,y]
take F . n ; :: thesis: S3[n,F . n]
thus S3[n,F . n] by A21; :: thesis: verum
end;
suppose A22: n = H . (k + 1) ; :: thesis: ex y being Element of ExtREAL st S3[n,y]
take 0. ; :: thesis: S3[n, 0. ]
thus S3[n, 0. ] by A22; :: thesis: verum
end;
end;
end;
consider G1 being Function of NAT ,ExtREAL such that
A23: for n being Element of NAT holds S3[n,G1 . n] from FUNCT_2:sch 3(A20);
 for n being Element of NAT holds 0. <= G1 . n
proof
let n be Element of NAT ; :: thesis: 0. <= G1 . n
per cases ( n <> H . (k + 1) or n = H . (k + 1) ) ;
suppose n <> H . (k + 1) ; :: thesis: 0. <= G1 . n
then G1 . n = F . n by A23;
hence 0. <= G1 . n by A14, SUPINF_2:58; :: thesis: verum
end;
suppose n = H . (k + 1) ; :: thesis: 0. <= G1 . n
hence 0. <= G1 . n by A23; :: thesis: verum
end;
end;
end;
then A24: G1 is nonnegative by SUPINF_2:58;
reconsider GG0 = On (G0 * H) as Function of NAT ,ExtREAL ;
G0 * H is nonnegative by A19, MEASURE1:54;
then A25: GG0 is nonnegative by Th8;
reconsider n = k + 1 as Element of S by A12;
A26: GG0 . n = (G0 * H) . n by Def1
.= G0 . (H . n) by FUNCT_2:21
.= F . (H . n) by A18 ;
A27: for n being Element of NAT st n <> k + 1 holds
GG0 . n = 0.
proof
let n be Element of NAT ; :: thesis: ( n <> k + 1 implies GG0 . n = 0. )
assume A28: n <> k + 1 ; :: thesis: GG0 . n = 0.
per cases ( n in S or not n in S ) ;
suppose A29: n in S ; :: thesis: GG0 . n = 0.
then A30: GG0 . n = (G0 * H) . n by Def1
.= G0 . (H . n) by A29, FUNCT_2:21 ;
reconsider n = n as Element of S by A29;
not H . n = H . (k + 1) by A2, A12, A28, FUNCT_2:25;
hence GG0 . n = 0. by A18, A30; :: thesis: verum
end;
end;
end;
set GG1 = On (G1 * H);
G1 * H is nonnegative by A24, MEASURE1:54;
then A31: On (G1 * H) is nonnegative by Th8;
A32: (On (G1 * H)) . (k + 1) = (G1 * H) . n by Def1
.= G1 . (H . n) by FUNCT_2:21
.= 0. by A23 ;
A33: for n being Element of NAT st n <> k + 1 & n in S holds
(On (G1 * H)) . n = F . (H . n)
proof
let n be Element of NAT ; :: thesis: ( n <> k + 1 & n in S implies (On (G1 * H)) . n = F . (H . n) )
assume A34: ( n <> k + 1 & n in S ) ; :: thesis: (On (G1 * H)) . n = F . (H . n)
then A35: (On (G1 * H)) . n = (G1 * H) . n by Def1
.= G1 . (H . n) by A34, FUNCT_2:21 ;
reconsider n = n as Element of S by A34;
not H . n = H . (k + 1) by A2, A12, A34, FUNCT_2:25;
hence (On (G1 * H)) . n = F . (H . n) by A23, A35; :: thesis: verum
end;
A36: for n being Element of NAT holds (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
proof
let n be Element of NAT ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
per cases ( n = k + 1 or n <> k + 1 ) ;
suppose A37: n = k + 1 ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
then (On (F * H)) . n = (F * H) . n by A12, Def1
.= F . (H . n) by A12, A37, FUNCT_2:21
.= (GG0 . n) + ((On (G1 * H)) . n) by A26, A32, A37, XXREAL_3:4 ;
hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; :: thesis: verum
end;
suppose A38: n <> k + 1 ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
now
per cases ( n in S or not n in S ) ;
suppose A39: n in S ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
A40: GG0 . n = 0. by A27, A38;
A41: (On (G1 * H)) . n = F . (H . n) by A33, A38, A39;
(On (F * H)) . n = (F * H) . n by A39, Def1
.= F . (H . n) by A39, FUNCT_2:21
.= (GG0 . n) + ((On (G1 * H)) . n) by A40, A41, XXREAL_3:4 ;
hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; :: thesis: verum
end;
suppose A42: not n in S ; :: thesis: (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n)
A43: GG0 . n = 0. by A27, A38;
A44: (On (G1 * H)) . n = 0. by A42, Def1;
(On (F * H)) . n = 0. by A42, Def1
.= (GG0 . n) + ((On (G1 * H)) . n) by A43, A44, XXREAL_3:4 ;
hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; :: thesis: verum
end;
end;
end;
hence (On (F * H)) . n = (GG0 . n) + ((On (G1 * H)) . n) ; :: thesis: verum
end;
end;
end;
A45: (Ser GG0) . (k + 1) = F . (H . (k + 1)) by A26, A27, Th10;
A46: (Ser G0) . (m0 + m1) = G0 . (H . (k + 1)) by A13, A18, Th10;
set v = H . n;
A47: G0 . (H . n) = F . (H . n) by A18;
A48: (Ser (On (G1 * H))) . (k + 1) = ((Ser (On (G1 * H))) . k) + ((On (G1 * H)) . (k + 1)) by SUPINF_2:63
.= (Ser (On (G1 * H))) . k by A32, XXREAL_3:4 ;
A49: (Ser (On (G1 * H))) . k <= (Ser G1) . m0 by A11, A24;
(Ser G1) . m0 <= (Ser G1) . (m0 + m1) by A24, Th9, NAT_1:11;
then A50: (Ser (On (G1 * H))) . (k + 1) <= (Ser G1) . (m0 + m1) by A48, A49, XXREAL_0:2;
for m being Element of NAT holds F . m = (G0 . m) + (G1 . m)
proof
let m be Element of NAT ; :: thesis: F . m = (G0 . m) + (G1 . m)
per cases ( m = H . (k + 1) or m <> H . (k + 1) ) ;
suppose A52: m = H . (k + 1) ; :: thesis: F . m = (G0 . m) + (G1 . m)
then A53: G0 . m = F . m by A18;
G1 . m = 0. by A23, A52;
hence F . m = (G0 . m) + (G1 . m) by A53, XXREAL_3:4; :: thesis: verum
end;
suppose A54: m <> H . (k + 1) ; :: thesis: F . m = (G0 . m) + (G1 . m)
then A55: G0 . m = 0. by A18;
G1 . m = F . m by A23, A54;
hence F . m = (G0 . m) + (G1 . m) by A55, XXREAL_3:4; :: thesis: verum
end;
end;
end;
then ( (Ser (On (F * H))) . (k + 1) = ((Ser GG0) . (k + 1)) + ((Ser (On (G1 * H))) . (k + 1)) & (Ser F) . (m0 + m1) = ((Ser G0) . (m0 + m1)) + ((Ser G1) . (m0 + m1)) ) by A19, A24, A25, A31, A36, Th3;
hence (Ser (On (F * H))) . (k + 1) <= (Ser F) . (m0 + m1) by A45, A46, A47, A50, XXREAL_3:38; :: thesis: verum
end;
suppose A56: not k + 1 in S ; :: thesis: S1[k + 1]
take m0 ; :: thesis: for F being Function of NAT ,ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . (k + 1) <= (Ser F) . m0
let F be Function of NAT ,ExtREAL ; :: thesis: ( F is nonnegative implies (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 )
assume A57: F is nonnegative ; :: thesis: (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0
A58: (On (F * H)) . (k + 1) = 0. by A56, Def1;
(Ser (On (F * H))) . (k + 1) = ((Ser (On (F * H))) . k) + ((On (F * H)) . (k + 1)) by SUPINF_2:63
.= (Ser (On (F * H))) . k by A58, XXREAL_3:4 ;
hence (Ser (On (F * H))) . (k + 1) <= (Ser F) . m0 by A11, A57; :: thesis: verum
end;
end;
end;
A59: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A3, A10);
 for x being ext-real number st x in rng (Ser (On (G * H))) holds
ex y being ext-real number st
( y in rng (Ser G) & x <= y )
proof
let x be ext-real number ; :: thesis: ( x in rng (Ser (On (G * H))) implies ex y being ext-real number st
( y in rng (Ser G) & x <= y ) )
assume A60: x in rng (Ser (On (G * H))) ; :: thesis: ex y being ext-real number st
( y in rng (Ser G) & x <= y )
ex y being ext-real number st
( y in rng (Ser G) & x <= y )
proof
consider n being set such that
A61: ( n in dom (Ser (On (G * H))) & x = (Ser (On (G * H))) . n ) by A60, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A61;
consider m being Element of NAT such that
A62: for F being Function of NAT ,ExtREAL st F is nonnegative holds
(Ser (On (F * H))) . n <= (Ser F) . m by A59;
take (Ser G) . m ; :: thesis: ( (Ser G) . m in rng (Ser G) & x <= (Ser G) . m )
( dom (Ser G) = NAT & m in NAT ) by FUNCT_2:def 1;
hence ( (Ser G) . m in rng (Ser G) & x <= (Ser G) . m ) by A1, A61, A62, FUNCT_1:def 5; :: thesis: verum
end;
hence ex y being ext-real number st
( y in rng (Ser G) & x <= y ) ; :: thesis: verum
end;
then A63: sup (rng (Ser (On (G * H)))) <= sup (rng (Ser G)) by XXREAL_2:63;
SUM G = sup (rng (Ser G)) by SUPINF_2:def 23;
hence SUM (On (G * H)) <= SUM G by A63, SUPINF_2:def 23; :: thesis: verum