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 n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & f2 is without-infty & f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) )
let f2 be Function of [:NAT,NAT:],ExtREAL; :: thesis: for c being Real st 0 <= c & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) holds
( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & f2 is without-infty & f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) )
let c be Real; :: thesis: ( 0 <= c & ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) ) & ( for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ) implies ( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & f2 is without-infty & f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) ) )
assume that
A1: 0 <= c and
A2: for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f1 . (n1,m1) <= f1 . (n2,m2) and
A3: for n, m being Nat holds f2 . (n,m) = c * (f1 . (n,m)) ; :: thesis: ( ( for n1, m1, n2, m2 being Nat st n1 <= n2 & m1 <= m2 holds
f2 . (n1,m1) <= f2 . (n2,m2) ) & f2 is without-infty & f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) )
A5: sup (rng f1) = P-lim f1 by A2, Th96;

hereby :: thesis: ( f2 is without-infty & f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) )

let n1, m1, n2, m2 be Nat; :: thesis: ( n1 <= n2 & m1 <= m2 implies f2 . (n1,m1) <= f2 . (n2,m2) )
assume ( n1 <= n2 & m1 <= m2 ) ; :: thesis: f2 . (n1,m1) <= f2 . (n2,m2)
then c * (f1 . (n1,m1)) <= c * (f1 . (n2,m2)) by A1, A2, XXREAL_3:71;
then f2 . (n1,m1) <= c * (f1 . (n2,m2)) by A3;
hence f2 . (n1,m1) <= f2 . (n2,m2) by A3; :: thesis: verum

end;

thus f2 is without-infty by A1, A3, Th104; :: thesis: ( f2 is P-convergent & P-lim f2 = sup (rng f2) & P-lim f2 = c * (P-lim f1) )
thus ( f2 is P-convergent & P-lim f2 = sup (rng f2) ) by A6, Th96; :: thesis: P-lim f2 = c * (P-lim f1)
sup (rng f2) = P-lim f2 by A6, Th96;
hence P-lim f2 = c * (P-lim f1) by A1, A3, A5, Th104; :: thesis: verum