let f1 be without-infty Function of [:NAT,NAT:],ExtREAL; :: thesis: for f2 being Function of [:NAT,NAT:],ExtREAL
for c being Real st 0 <= c & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( sup (rng f2) = c * (sup (rng f1)) & f2 is without-infty )
let f2 be Function of [:NAT,NAT:],ExtREAL; :: thesis: for c being Real st 0 <= c & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( sup (rng f2) = c * (sup (rng f1)) & f2 is without-infty )
let c be Real; :: thesis: ( 0 <= c & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) implies ( sup (rng f2) = c * (sup (rng f1)) & f2 is without-infty ) )
assume that
A1: 0 <= c and
A3: for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ; :: thesis: ( sup (rng f2) = c * (sup (rng f1)) & f2 is without-infty )
A6: ( dom f1 = [:NAT,NAT:] & dom f2 = [:NAT,NAT:] ) by FUNCT_2:def 1;
C6: now :: thesis: not -infty in rng f2
assume -infty in rng f2 ; :: thesis: contradiction
then consider z being object such that
C1: ( z in dom f2 & -infty = f2 . z ) by FUNCT_1:def 3;
consider n, m being object such that
C2: ( n in NAT & m in NAT & z = [n,m] ) by C1, ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by C2;
f2 . (n,m) = -infty by C1, C2;
then C3: c * (f1 . (n,m)) = -infty by A3;
then C4: ( f1 . (n,m) = -infty or f1 . (n,m) = +infty ) by XXREAL_3:70;
z in [:NAT,NAT:] by C1;
then [n,m] in dom f1 by C2, FUNCT_2:def 1;
then -infty in rng f1 by A1, C3, C4, FUNCT_1:3;
hence contradiction by MESFUNC5:def 3; :: thesis: verum
end;
then C6a: f2 is without-infty by MESFUNC5:def 3;
now :: thesis: sup (rng f2) = c * (sup (rng f1))
per cases ( sup (rng f1) in REAL or sup (rng f1) = +infty ) by Lm8;
suppose A4: sup (rng f1) in REAL ; :: thesis: sup (rng f2) = c * (sup (rng f1))
A5: for y being UpperBound of rng f2 holds c * (sup (rng f1)) <= y
proof
let y be UpperBound of rng f2; :: thesis: c * (sup (rng f1)) <= y
reconsider y = y as R_eal by XXREAL_0:def 1;
per cases ( c = 0 or c <> 0 ) ;
suppose A8: c = 0 ; :: thesis: c * (sup (rng f1)) <= y
[1,1] in [:NAT,NAT:] by ZFMISC_1:87;
then f2 . (1,1) <= y by A6, FUNCT_1:3, XXREAL_2:def 1;
then c * (f1 . (1,1)) <= y by A3;
hence c * (sup (rng f1)) <= y by A8; :: thesis: verum
end;
suppose A10: c <> 0 ; :: thesis: c * (sup (rng f1)) <= y
now :: thesis: for x being ExtReal st x in rng f1 holds
x <= y / c
let x be ExtReal; :: thesis: ( x in rng f1 implies x <= y / c )
assume x in rng f1 ; :: thesis: x <= y / c
then consider z being object such that
A11: ( z in dom f1 & x = f1 . z ) by FUNCT_1:def 3;
consider n, m being object such that
A12: ( n in NAT & m in NAT & z = [n,m] ) by A11, ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by A12;
A14: f2 . (n,m) in rng f2 by A11, A12, A6, FUNCT_1:3;
f2 . (n,m) = c * (f1 . (n,m)) by A3;
then (c * (f1 . (n,m))) / c <= y / c by A1, A10, A14, XXREAL_2:def 1, XXREAL_3:79;
hence x <= y / c by A10, A11, A12, XXREAL_3:88; :: thesis: verum
end;
then B14: y / c is UpperBound of rng f1 by XXREAL_2:def 1;
per cases ( y = +infty or y in REAL ) by A15, XXREAL_0:14;
suppose y = +infty ; :: thesis: c * (sup (rng f1)) <= y
hence c * (sup (rng f1)) <= y by XXREAL_0:4; :: thesis: verum
end;
suppose y in REAL ; :: thesis: c * (sup (rng f1)) <= y
then reconsider ry = y as Real ;
reconsider SE1 = sup (rng f1) as Real by A4;
y / c = ry / c by EXTREAL1:2;
then SE1 * c <= ry by A1, A10, B14, XXREAL_2:def 3, XREAL_1:83;
hence c * (sup (rng f1)) <= y by XXREAL_3:def 5; :: thesis: verum
end;
end;
end;
end;
end;
now :: thesis: for x being ExtReal st x in rng f2 holds
x <= c * (sup (rng f1))
let x be ExtReal; :: thesis: ( x in rng f2 implies x <= c * (sup (rng f1)) )
assume x in rng f2 ; :: thesis: x <= c * (sup (rng f1))
then consider z2 being object such that
A22: ( z2 in dom f2 & x = f2 . z2 ) by FUNCT_1:def 3;
consider n2, m2 being object such that
A23: ( n2 in NAT & m2 in NAT & z2 = [n2,m2] ) by A22, ZFMISC_1:def 2;
reconsider n2 = n2, m2 = m2 as Element of NAT by A23;
A24: sup (rng f1) is UpperBound of rng f1 by XXREAL_2:def 3;
[n2,m2] in dom f1 by A6, ZFMISC_1:87;
then A25: f1 . (n2,m2) <= sup (rng f1) by A24, XXREAL_2:def 1, FUNCT_1:3;
x = f2 . (n2,m2) by A22, A23;
then x = c * (f1 . (n2,m2)) by A3;
hence x <= c * (sup (rng f1)) by A1, A25, XXREAL_3:71; :: thesis: verum
end;
then c * (sup (rng f1)) is UpperBound of rng f2 by XXREAL_2:def 1;
hence sup (rng f2) = c * (sup (rng f1)) by A5, XXREAL_2:def 3; :: thesis: verum
end;
suppose A30: sup (rng f1) = +infty ; :: thesis: sup (rng f2) = c * (sup (rng f1))
per cases ( c = 0 or c <> 0 ) ;
suppose A27: c = 0 ; :: thesis: sup (rng f2) = c * (sup (rng f1))
A28: now :: thesis: for n, m being Nat holds f2 . (n,m) = 0
let n, m be Nat; :: thesis: f2 . (n,m) = 0
f2 . (n,m) = c * (f1 . (n,m)) by A3;
hence f2 . (n,m) = 0 by A27; :: thesis: verum
end;
then P-lim f2 = sup (rng f2) by Th102;
hence sup (rng f2) = c * (sup (rng f1)) by A27, A28, Th102; :: thesis: verum
end;
suppose A29: c <> 0 ; :: thesis: sup (rng f2) = c * (sup (rng f1))
A34: now :: thesis: for k being Real st 0 < k holds
ex n, m being Nat st not f2 . (n,m) <= k
let k be Real; :: thesis: ( 0 < k implies ex n, m being Nat st not f2 . (n,m) <= k )
reconsider k1 = k as Real ;
assume C5: 0 < k ; :: thesis: not for n, m being Nat holds f2 . (n,m) <= k
then consider n, m being Nat such that
A31: k / c < f1 . (n,m) by A1, A29, A30, Th101;
C10: f2 . (n,m) = c * (f1 . (n,m)) by A3;
( n in NAT & m in NAT ) by ORDINAL1:def 12;
then [n,m] in dom f2 by A6, ZFMISC_1:87;
then C3: f2 . (n,m) <> -infty by C6, FUNCT_1:3;
now :: thesis: k < f2 . (n,m)
per cases ( f2 . (n,m) in REAL or f2 . (n,m) = +infty ) by C3, XXREAL_0:14;
suppose C7: f2 . (n,m) in REAL ; :: thesis: k < f2 . (n,m)
( f1 . (n,m) > 0 & 0 >= -infty ) by A1, C5, A31;
then C9: ( f1 . (n,m) in REAL or f1 . (n,m) = +infty ) by XXREAL_0:14;
now :: thesis: not f1 . (n,m) = +infty
assume f1 . (n,m) = +infty ; :: thesis: contradiction
then c * (f1 . (n,m)) = +infty by A1, A29, XXREAL_3:def 5;
hence contradiction by A3, C7; :: thesis: verum
end;
then reconsider ES1 = f1 . (n,m) as Real by C9;
k < c * ES1 by A1, A29, A31, XREAL_1:77;
hence k < f2 . (n,m) by C10, XXREAL_3:def 5; :: thesis: verum
end;
suppose f2 . (n,m) = +infty ; :: thesis: k < f2 . (n,m)
hence k < f2 . (n,m) by XREAL_0:def 1, XXREAL_0:9; :: thesis: verum
end;
end;
end;
hence not for n, m being Nat holds f2 . (n,m) <= k ; :: thesis: verum
end;
c * (sup (rng f1)) = +infty by A1, A29, A30, XXREAL_3:def 5;
hence sup (rng f2) = c * (sup (rng f1)) by C6a, A34, Th101; :: thesis: verum
end;
end;
end;
end;
end;
hence sup (rng f2) = c * (sup (rng f1)) ; :: thesis: f2 is without-infty
thus f2 is without-infty by C6, MESFUNC5:def 3; :: thesis: verum