:: Scalar Multiple of Riemann Definite Integral
:: by Noboru Endou , Katsumi Wasaki and Yasunari Shidama
::
:: Received December 7, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, FINSEQ_1, INTEGRA1, SEQ_4, XXREAL_0,
XXREAL_1, VALUED_0, RELAT_1, ARYTM_3, FUNCT_1, CARD_1, NAT_1, CLASSES1,
FINSEQ_5, ARYTM_1, ORDINAL4, XBOOLE_0, JORDAN3, MEMBERED, MEMBER_1,
TARSKI, PARTFUN1, XXREAL_2, VALUED_1, MEASURE7, CARD_3, SEQ_1, INTEGRA2,
MEASURE5, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XXREAL_0,
XREAL_0, XXREAL_2, XXREAL_3, MEMBERED, MEMBER_1, XCMPLX_0, REAL_1, NAT_1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, RFUNCT_1,
RVSUM_1, INTEGRA1, VALUED_0, VALUED_1, SEQ_1, COMSEQ_2, SEQ_2, SEQ_4,
FINSEQ_6, RCOMP_1, FINSEQ_5, CLASSES1, RFINSEQ, MEASURE5, MEASURE6;
constructors PARTFUN1, REAL_1, NAT_1, SEQM_3, VALUED_0, RFUNCT_1, RFINSEQ,
BINARITH, FINSEQ_5, FINSEQ_6, INTEGRA1, XXREAL_2, NAT_D, RVSUM_1, SEQ_4,
CLASSES1, RELSET_1, SEQ_2, MEMBER_1, MEASURE6, COMSEQ_2;
registrations RELAT_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED,
FINSEQ_1, INTEGRA1, VALUED_0, VALUED_1, XXREAL_2, CARD_1, SEQ_2,
RELSET_1, XXREAL_3, MEMBER_1, MEASURE5, NAT_1, RFINSEQ;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, XXREAL_2;
equalities XBOOLE_0, VALUED_1, RELAT_1;
expansions TARSKI, XBOOLE_0, XXREAL_2;
theorems SEQ_4, SUBSET_1, PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FINSEQ_1,
RVSUM_1, NEWTON, RCOMP_1, NAT_1, RFINSEQ, CARD_1, FINSEQ_5, FINSEQ_3,
RELAT_1, FUNCT_2, XBOOLE_0, XBOOLE_1, XCMPLX_1, XREAL_1, XXREAL_0,
ORDINAL1, MEMBERED, VALUED_1, XXREAL_2, TARSKI, SEQM_3, CLASSES1,
FINSEQ_6, MEMBER_1, XXREAL_3, VALUED_0;
schemes SUBSET_1, SEQ_1, NAT_1;
begin :: Lemmas of Finite Sequence
reserve a,b,r,x,y for Real,
i,j,k,n for Nat,
x1 for set;
theorem
for A be non empty closed_interval Subset of REAL, x being Real holds
x in A iff lower_bound A <= x & x <= upper_bound A
proof
let A be non empty closed_interval Subset of REAL;
let x be Real;
hereby
assume x in A;
then x in [.lower_bound A,upper_bound A.] by INTEGRA1:4;
then x in {a: lower_bound A <= a & a <= upper_bound A} by RCOMP_1:def 1;
then ex a st a=x & lower_bound A <= a & a <= upper_bound A;
hence lower_bound A <= x & x <= upper_bound A;
end;
assume
A1: lower_bound A <= x & x <= upper_bound A;
x in {a: lower_bound A <= a & a <= upper_bound A} by A1;
then x in [.lower_bound A,upper_bound A.] by RCOMP_1:def 1;
hence thesis by INTEGRA1:4;
end;
LM:for p be real-valued FinSequence st
for n be Nat st n in dom p & n+1 in dom p holds p.n <= p.(n+1)
holds
for i,j st i in dom p & j in dom p & i <= j holds p.i <= p.j
proof
let p be real-valued FinSequence;
assume
A0: for n be Nat st n in dom p & n+1 in dom p holds p.n <= p.(n+1);
let i,j;
assume
A1: i in dom p;
defpred P[Nat] means
for i,j st j = i + $1 & i in dom p & j in dom p holds p.i <= p.j;
assume
A2: j in dom p;
A3: for k st P[k] holds P[k+1]
proof
let k;
assume
A4: P[k];
P[k+1]
proof
let i,j;
reconsider l=i+k as Nat;
assume j=i+(k+1); then
A5: j=l+1;
assume
A6: i in dom p;
then 1 <= i by FINSEQ_3:25; then
A7: 1+0 <= l by XREAL_1:7;
assume
A8: j in dom p;
then j <= len p by FINSEQ_3:25;
then l < len p by A5,NAT_1:13; then
A9: l in dom p by A7,FINSEQ_3:25; then
A10: p.i <= p.l by A4,A6;
p.l <= p.j by A0,A8,A5,A9;
hence thesis by A10,XXREAL_0:2;
end;
hence thesis;
end;
A11: P[0];
A12: for k holds P[k] from NAT_1:sch 2(A11,A3);
assume i <= j;
then consider n being Nat such that
A13: j = i + n by NAT_1:10;
reconsider n as Nat;
j = i + n by A13;
hence thesis by A1,A2,A12;
end;
definition
let IT be real-valued FinSequence;
redefine attr IT is non-decreasing means :Def1: :: redefines non-decreasing (VALUED_0, definition)
for n be Nat st n in dom IT & n+1 in dom IT holds IT.n <= IT.(n+1);
compatibility
proof
thus IT is non-decreasing implies
for n st n in dom IT & n+1 in dom IT holds
IT.n <= IT.(n+1) by NAT_1:11,VALUED_0:def 15;
assume for n be Nat st n in dom IT & n+1 in dom IT
holds IT.n <= IT.(n+1);
then for e1,e2 be ExtReal st e1 in dom IT & e2 in dom IT & e1 <= e2
holds IT.e1 <= IT.e2 by LM;
hence thesis by VALUED_0:def 15;
end;
end;
theorem
for p be non-decreasing real-valued FinSequence, i,j st
i in dom p & j in dom p & i <= j holds p.i <= p.j
proof
let p be non-decreasing real-valued FinSequence;
for n be Nat st n in dom p & n+1 in dom p holds p.n <= p.(n+1) by Def1;
hence thesis by LM;
end;
theorem
for p being real-valued FinSequence
ex q be non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent
proof
let p be real-valued FinSequence;
consider q being non-increasing FinSequence of REAL such that
A1: p,q are_fiberwise_equipotent by RFINSEQ:22;
for n be Nat st n in dom Rev q & n+1 in dom Rev q holds
(Rev q).n <= (Rev q).(n+1)
proof
let n;
assume that
A2: n in dom Rev q and
A3: n+1 in dom Rev q;
(Rev q).n <= (Rev q).(n+1)
proof
n in Seg len Rev q by A2,FINSEQ_1:def 3;
then 1 <= n by FINSEQ_1:1;
then n - 1 >= 0 by XREAL_1:48;
then len q + 0 <= len q + (n - 1) by XREAL_1:7;
then
A4: len q - (n - 1) <= len q by XREAL_1:20;
n in Seg len Rev q by A2,FINSEQ_1:def 3;
then n in Seg len q by FINSEQ_5:def 3;
then n <= len q by FINSEQ_1:1;
then consider m being Nat such that
A5: len q = n + m by NAT_1:10;
reconsider m as Nat;
m + 1 = len q - n + 1 & 1 <= len q - n + 1 by A5,NAT_1:11;
then len q - n + 1 in Seg len q by A4,FINSEQ_1:1;
then
A6: len q - n + 1 in dom q by FINSEQ_1:def 3;
set x=(Rev q).n, y=(Rev q).(n+1);
A7: len q - (n+1) + 1 = len q-n;
len q <= len q + n by NAT_1:11;
then
A8: len q - (n+1) + 1 <= len q by A7,XREAL_1:20;
n+1 in Seg len Rev q by A3,FINSEQ_1:def 3;
then n+1 in Seg len q by FINSEQ_5:def 3;
then n+1 <= len q by FINSEQ_1:1;
then 1 <= len q - (n+1) + 1 by A7,XREAL_1:19;
then len q - (n+1) + 1 in Seg len q by A5,A8,FINSEQ_1:1;
then
A9: len q - (n+1) + 1 in dom q by FINSEQ_1:def 3;
x = q.(len q - n + 1) & y = q.(len q - (n+1) + 1)
by A2,A3,FINSEQ_5:def 3;
hence thesis by A6,A9,RFINSEQ:def 3;
end;
hence thesis;
end;
then reconsider r=Rev q as non-decreasing FinSequence of REAL by Def1;
take r;
p,Rev q are_fiberwise_equipotent
proof
defpred P[Nat] means
for p be real-valued FinSequence,
q be non-increasing real-valued FinSequence
st len p = $1 & p,q are_fiberwise_equipotent
holds p,Rev q are_fiberwise_equipotent;
A10: for k st P[k] holds P[k+1]
proof
let k;
assume
A11: P[k];
P[k+1]
proof
let p be real-valued FinSequence;
let q be non-increasing real-valued FinSequence;
consider q1 being non-increasing FinSequence of REAL such that
A12: p,q1 are_fiberwise_equipotent by RFINSEQ:22;
reconsider kk= k as Element of NAT by ORDINAL1:def 12;
reconsider q1k = q1|kk as non-increasing FinSequence of REAL
by RFINSEQ:20;
A13: Rev(q1k)^<*q1.(k+1)*>,<*q1.(k+1)*>^Rev(q1k)
are_fiberwise_equipotent by RFINSEQ:2;
assume
A14: len p = k+1;
then
A15: len q1= k+1 by A12,RFINSEQ:3;
len p = len q1 by A12,RFINSEQ:3;
then len(q1|k) = k by A14,FINSEQ_1:59,NAT_1:11;
then q1|k,Rev(q1k) are_fiberwise_equipotent by A11;
then (q1|k)^<*q1.(k+1)*>,Rev(q1k)^<*q1.(k+1)*>
are_fiberwise_equipotent by RFINSEQ:1;
then q1,Rev(q1k)^<*q1.(k+1)*> are_fiberwise_equipotent by A15,RFINSEQ:7
;
then
A16: q1,<*q1.(k+1)*>^Rev(q1k) are_fiberwise_equipotent by A13,CLASSES1:76;
A17: <*q1.(k+1)*>^Rev(q1k) = Rev((q1|k)^<*q1.(k+1)*>) by FINSEQ_5:63
.= Rev(q1) by A15,RFINSEQ:7;
assume p,q are_fiberwise_equipotent;
then q=q1 by A12,CLASSES1:76,RFINSEQ:23;
hence thesis by A12,A16,A17,CLASSES1:76;
end;
hence thesis;
end;
A18: len p = len p;
A19: P[0]
proof
let p be real-valued FinSequence;
let q be non-increasing real-valued FinSequence;
assume
A20: len p = 0;
assume p,q are_fiberwise_equipotent;
then len q = 0 by A20,RFINSEQ:3;
then len Rev q = 0 by FINSEQ_5:def 3;
then Rev q = {};
then
A21: rng Rev q = {};
p = {} by A20;
then
A22: rng p = {};
for x be object holds card Coim(p,x) = card Coim(Rev q,x)
proof
let x be object;
card (p"{x}) = 0 by A22,CARD_1:27,FUNCT_1:72;
hence thesis by A21,CARD_1:27,FUNCT_1:72;
end;
hence thesis by CLASSES1:def 10;
end;
for k holds P[k] from NAT_1:sch 2(A19,A10);
hence thesis by A1,A18;
end;
hence thesis;
end;
theorem
for D be non empty set, f be FinSequence of D, k1,k2,k3 be Nat
st 1<=k1 & k3<=len f & k1<=k2 & k2<k3
holds mid(f,k1,k2)^mid(f,k2+1,k3)=mid(f,k1,k3)
proof
let D be non empty set;
let f be FinSequence of D;
let k1,k2,k3 be Nat;
assume that
A1: 1<=k1 and
A2: k3<=len f and
A3: k1<=k2 and
A4: k2<k3;
A5: k2 <= len f by A2,A4,XXREAL_0:2;
then
A6: k1<=len f by A3,XXREAL_0:2;
1<=k2 & k2<=len f by A1,A2,A3,A4,XXREAL_0:2;
then
A7: len mid(f,k1,k2)=k2-'k1+1 by A1,A3,A6,FINSEQ_6:118
.=k2-k1+1 by A3,XREAL_1:233;
A8: 1 <= k2 by A1,A3,XXREAL_0:2;
then
A9: 1<=k3 by A4,XXREAL_0:2;
A10: k1<k3 by A3,A4,XXREAL_0:2;
A11: 1<=k2+1 by A8,NAT_1:13;
A12: k2+1<=k3 by A4,NAT_1:13;
then k2+1<=len f by A2,XXREAL_0:2;
then
A13: len mid(f,k2+1,k3)=k3-'(k2+1)+1 by A2,A9,A12,A11,FINSEQ_6:118
.=k3-(k2+1)+1 by A12,XREAL_1:233
.=k3-k2;
then
A14: len(mid(f,k1,k2)^mid(f,k2+1,k3))=(k2-k1+1)+(k3-k2) by A7,FINSEQ_1:22
.=k3-k1+1;
A15: 1<=k2+1 by A8,NAT_1:13;
A16: for k be Nat st 1<=k & k<=len(mid(f,k1,k2)^mid(f,k2+1,k3)) holds (mid(f
,k1,k2)^mid(f,k2+1,k3)).k = mid(f,k1,k3).k
proof
let k be Nat;
assume
A17: 1<=k & k<=len(mid(f,k1,k2)^mid(f,k2+1,k3));
then k in Seg len(mid(f,k1,k2)^mid(f,k2+1,k3)) by FINSEQ_1:1;
then
A18: k in dom(mid(f,k1,k2)^mid(f,k2+1,k3)) by FINSEQ_1:def 3;
now
per cases by A18,FINSEQ_1:25;
suppose
A19: k in dom mid(f,k1,k2);
then
A20: k in Seg len mid(f,k1,k2) by FINSEQ_1:def 3;
then
A21: 1 <= k by FINSEQ_1:1;
A22: k <= k2-k1+1 by A7,A20,FINSEQ_1:1;
k2-k1 <= k3-k1 by A4,XREAL_1:9;
then k2-k1+1 <= k3-k1+1 by XREAL_1:6;
then
A23: k <= k3-k1+1 by A22,XXREAL_0:2;
(mid(f,k1,k2)^mid(f,k2+1,k3)).k=mid(f,k1,k2).k by A19,FINSEQ_1:def 7
.=f.(k-1+k1) by A1,A3,A5,A21,A22,FINSEQ_6:122;
hence thesis by A1,A2,A10,A21,A23,FINSEQ_6:122;
end;
suppose
ex n be Nat st n in dom mid(f,k2+1,k3)&k=len mid(f,k1,k2)+n;
then consider n be Nat such that
A24: n in dom mid(f,k2+1,k3) and
A25: k=len mid(f,k1,k2)+n;
A26: mid(f,k1,k3).k=f.(k2-(k1-1)+n+k1-1) by A1,A2,A10,A7,A14,A17,A25,
FINSEQ_6:122
.=f.(n+k2);
n in Seg len mid(f,k2+1,k3) by A24,FINSEQ_1:def 3;
then
A27: 1 <= n & n <= k3-(k2+1)+1 by A13,FINSEQ_1:1;
(mid(f,k1,k2)^mid(f,k2+1,k3)).k=mid(f,k2+1,k3).n by A24,A25,
FINSEQ_1:def 7
.=f.(n+(k2+1)-1) by A2,A15,A12,A27,FINSEQ_6:122
.=f.(n+k2+0);
hence thesis by A26;
end;
end;
hence thesis;
end;
len mid(f,k1,k3)=k3-'k1+1 by A1,A2,A6,A9,A10,FINSEQ_6:118
.=k3-k1+1 by A3,A4,XREAL_1:233,XXREAL_0:2;
hence thesis by A14,A16,FINSEQ_1:14;
end;
begin :: Scalar Product of Real Subset
definition
let A be real-membered set;
let x be Real;
redefine func x ** A -> Subset of REAL; :: redefines ** (MEMBER_1, definition)
coherence by MEMBERED:3;
end;
theorem
for X,Y be non empty set, f be PartFunc of X,REAL st
f|X is bounded_above & Y c= X holds f|Y|Y is bounded_above
proof
let X,Y be non empty set;
let f be PartFunc of X,REAL;
assume f|X is bounded_above;
then consider a be Real such that
A1: for x being object st x in X /\ dom f holds a>=f.x by RFUNCT_1:70;
assume
A2: Y c= X;
for x being object st x in Y /\ dom (f|Y) holds a>=(f|Y).x
proof
let x be object;
A3: dom f /\ Y c= dom f /\ X by A2,XBOOLE_1:26;
assume x in Y /\ dom (f|Y);
then
A4: x in dom (f|Y) by XBOOLE_0:def 4;
then x in dom f /\ Y by RELAT_1:61;
then a >= f.x by A1,A3;
hence thesis by A4,FUNCT_1:47;
end;
hence thesis by RFUNCT_1:70;
end;
theorem
for X,Y be non empty set, f be PartFunc of X,REAL st
f|X is bounded_below & Y c= X holds f|Y|Y is bounded_below
proof
let X,Y be non empty set;
let f be PartFunc of X,REAL;
assume f|X is bounded_below;
then consider a be Real such that
A1: for x being object st x in X /\ dom f holds f.x>=a by RFUNCT_1:71;
assume
A2: Y c= X;
for x being object st x in Y /\ dom (f|Y) holds (f|Y).x>=a
proof
let x be object;
A3: dom f /\ Y c= dom f /\ X by A2,XBOOLE_1:26;
assume x in Y /\ dom (f|Y);
then
A4: x in dom (f|Y) by XBOOLE_0:def 4;
then x in dom f /\ Y by RELAT_1:61;
then a <= f.x by A1,A3;
hence thesis by A4,FUNCT_1:47;
end;
hence thesis by RFUNCT_1:71;
end;
theorem
for X being real-membered set, a being Real holds
X is empty iff a ** X is empty;
theorem Th8:
for X be Subset of REAL holds r**X = {r*x : x in X}
proof
let X be Subset of REAL;
thus r**X c= {r*x : x in X}
proof
let y be object;
assume y in r**X;
then consider z being Element of ExtREAL such that
A1: y = r * z & z in X by MEMBER_1:188;
reconsider z1 = z as Element of REAL by A1;
y = r * z1 by A1,XXREAL_3:def 5;
hence thesis by A1;
end;
let y be object;
assume y in {r*x : x in X};
then consider z being Real such that
A2:y = r * z & z in X;
thus thesis by A2,MEMBER_1:193;
end;
theorem
for X be non empty Subset of REAL st X is bounded_above & 0<=r holds
r**X is bounded_above
proof
let X be non empty Subset of REAL;
assume that
A1: X is bounded_above and
A2: 0<=r;
consider b be Real such that
A3: b is UpperBound of X by A1;
A4: for x be Real st x in X holds x <= b by A3,XXREAL_2:def 1;
r*b is UpperBound of r**X
proof
let y be ExtReal;
assume y in r**X;
then y in {r*x : x in X} by Th8;
then consider x such that
A5: y=r*x and
A6: x in X;
x <= b by A4,A6;
hence thesis by A2,A5,XREAL_1:64;
end;
hence thesis;
end;
theorem
for X be non empty Subset of REAL st X is bounded_above & r<=0 holds
r**X is bounded_below
proof
let X be non empty Subset of REAL;
assume that
A1: X is bounded_above and
A2: r<=0;
consider b be Real such that
A3: b is UpperBound of X by A1;
A4: for x be Real st x in X holds x <= b by A3,XXREAL_2:def 1;
r*b is LowerBound of r**X
proof
let y be ExtReal;
assume y in r**X;
then y in {r*x : x in X} by Th8;
then ex x st y=r*x & x in X;
hence thesis by A2,A4,XREAL_1:65;
end;
hence thesis;
end;
theorem
for X be non empty Subset of REAL st X is bounded_below & 0<=r holds
r**X is bounded_below
proof
let X be non empty Subset of REAL;
assume that
A1: X is bounded_below and
A2: 0<=r;
consider b be Real such that
A3: b is LowerBound of X by A1;
A4: for x be Real st x in X holds b <= x by A3,XXREAL_2:def 2;
r*b is LowerBound of r**X
proof
let y be ExtReal;
assume y in r**X;
then y in {r*x : x in X} by Th8;
then ex x st y=r*x & x in X;
hence thesis by A2,A4,XREAL_1:64;
end;
hence thesis;
end;
theorem
for X be non empty Subset of REAL st X is bounded_below & r<=0 holds
r**X is bounded_above
proof
let X be non empty Subset of REAL;
assume that
A1: X is bounded_below and
A2: r<=0;
consider b be Real such that
A3: b is LowerBound of X by A1;
A4: for x be Real st x in X holds b <= x by A3,XXREAL_2:def 2;
r*b is UpperBound of r**X
proof
let y be ExtReal;
assume y in r**X;
then y in {r*x : x in X} by Th8;
then consider x such that
A5: y=r*x and
A6: x in X;
b <= x by A4,A6;
hence thesis by A2,A5,XREAL_1:65;
end;
hence thesis;
end;
theorem Th13:
for X be non empty Subset of REAL st X is bounded_above & 0<=r
holds upper_bound(r**X) = r*(upper_bound X)
proof
let X be non empty Subset of REAL;
assume that
A1: X is bounded_above and
A2: 0<=r;
A3: for a be Real st a in r**X holds a <= r*(upper_bound X)
proof
let a be Real;
assume a in r**X;
then a in {r*x : x in X} by Th8;
then consider x such that
A4: a=r*x and
A5: x in X;
x <= upper_bound X by A1,A5,SEQ_4:def 1;
hence thesis by A2,A4,XREAL_1:64;
end;
for b be Real st for a be Real st a in r**X holds a <= b
holds r*(upper_bound X) <= b
proof
consider x being Element of REAL such that
A6: x in X by SUBSET_1:4;
let b be Real;
assume
A7: for a be Real st a in r**X holds a <= b;
reconsider x as Real;
r*x in {r*y : y in X} by A6;
then
A8: r*x in r**X by Th8;
now
per cases by A2;
suppose
r=0;
hence thesis by A7,A8;
end;
suppose
A9: r>0;
for z be Real st z in X holds z <= b/r
proof
let z be Real;
assume z in X;
then r*z in {r*y : y in X};
then r*z in r**X by Th8;
hence thesis by A7,A9,XREAL_1:77;
end;
then upper_bound X <= b/r by SEQ_4:45;
then r*(upper_bound X) <= b/r*r by A9,XREAL_1:64;
hence thesis by A9,XCMPLX_1:87;
end;
end;
hence thesis;
end;
hence thesis by A3,SEQ_4:46;
end;
theorem Th14:
for X be non empty Subset of REAL st X is bounded_above & r<=0
holds lower_bound(r**X) = r*(upper_bound X)
proof
let X be non empty Subset of REAL;
assume that
A1: X is bounded_above and
A2: r<=0;
A3: for a be Real st a in r**X holds r*(upper_bound X) <= a
proof
let a be Real;
assume a in r**X;
then a in {r*x : x in X} by Th8;
then consider x such that
A4: a=r*x and
A5: x in X;
x <= upper_bound X by A1,A5,SEQ_4:def 1;
hence thesis by A2,A4,XREAL_1:65;
end;
for b be Real st for a be Real st a in r**X holds a >= b
holds r*(upper_bound X) >= b
proof
consider x being Element of REAL such that
A6: x in X by SUBSET_1:4;
let b be Real;
assume
A7: for a be Real st a in r**X holds a >= b;
reconsider x as Real;
r*x in {r*y : y in X} by A6;
then
A8: r*x in r**X by Th8;
now
per cases by A2;
suppose
r=0;
hence thesis by A7,A8;
end;
suppose
A9: r<0;
for z be Real st z in X holds z <= b/r
proof
let z be Real;
assume z in X;
then r*z in {r*y : y in X};
then r*z in r**X by Th8;
hence thesis by A7,A9,XREAL_1:80;
end;
then upper_bound X <= b/r by SEQ_4:45;
then r*(upper_bound X) >= b/r*r by A9,XREAL_1:65;
hence thesis by A9,XCMPLX_1:87;
end;
end;
hence thesis;
end;
hence thesis by A3,SEQ_4:44;
end;
theorem Th15:
for X be non empty Subset of REAL st X is bounded_below & 0<=r
holds lower_bound(r**X) = r*(lower_bound X)
proof
let X be non empty Subset of REAL;
assume that
A1: X is bounded_below and
A2: 0<=r;
A3: for a being Real st a in r**X holds r*(lower_bound X) <= a
proof
let a be Real;
assume a in r**X;
then a in {r*x : x in X} by Th8;
then consider x such that
A4: a=r*x and
A5: x in X;
lower_bound X <= x by A1,A5,SEQ_4:def 2;
hence thesis by A2,A4,XREAL_1:64;
end;
for b be Real st for a be Real st a in r**X holds a >= b
holds r*(lower_bound X) >= b
proof
consider x being Element of REAL such that
A6: x in X by SUBSET_1:4;
let b be Real;
assume
A7: for a be Real st a in r**X holds a >= b;
reconsider x as Real;
r*x in {r*y : y in X} by A6;
then
A8: r*x in r**X by Th8;
now
per cases by A2;
suppose
r=0;
hence thesis by A7,A8;
end;
suppose
A9: r>0;
for z be Real st z in X holds z >= b/r
proof
let z be Real;
assume z in X;
then r*z in {r*y : y in X};
then r*z in r**X by Th8;
hence thesis by A7,A9,XREAL_1:79;
end;
then lower_bound X >= b/r by SEQ_4:43;
then r*(lower_bound X) >= b/r*r by A9,XREAL_1:64;
hence thesis by A9,XCMPLX_1:87;
end;
end;
hence thesis;
end;
hence thesis by A3,SEQ_4:44;
end;
theorem Th16:
for X be non empty Subset of REAL st X is bounded_below & r<=0
holds upper_bound(r**X) = r*(lower_bound X)
proof
let X be non empty Subset of REAL;
assume that
A1: X is bounded_below and
A2: r<=0;
A3: for a be Real st a in r**X holds r*(lower_bound X) >= a
proof
let a be Real;
assume a in r**X;
then a in {r*x : x in X} by Th8;
then consider x such that
A4: a=r*x and
A5: x in X;
lower_bound X <= x by A1,A5,SEQ_4:def 2;
hence thesis by A2,A4,XREAL_1:65;
end;
for b be Real st for a be Real st a in r**X holds a <= b
holds r*(lower_bound X) <= b
proof
consider x being Element of REAL such that
A6: x in X by SUBSET_1:4;
let b be Real;
assume
A7: for a being Real st a in r**X holds a <= b;
reconsider x as Real;
r*x in {r*y : y in X} by A6;
then
A8: r*x in r**X by Th8;
now
per cases by A2;
suppose
r=0;
hence thesis by A7,A8;
end;
suppose
A9: r<0;
for z be Real st z in X holds z >= b/r
proof
let z be Real;
assume z in X;
then r*z in {r*y : y in X};
then r*z in r**X by Th8;
hence thesis by A7,A9,XREAL_1:78;
end;
then lower_bound X >= b/r by SEQ_4:43;
then r*(lower_bound X) <= b/r*r by A9,XREAL_1:65;
hence thesis by A9,XCMPLX_1:87;
end;
end;
hence thesis;
end;
hence thesis by A3,SEQ_4:46;
end;
begin :: Scalar Multiple of Integral
theorem Th17:
for X be non empty set, f be Function of X,REAL holds rng(r(#)f)
= r**rng f
proof
let X be non empty set;
let f be Function of X,REAL;
for y being Element of REAL holds y in r**rng f implies y in rng(r(#)f)
proof
let y be Element of REAL;
assume y in r**rng f;
then y in {r*b : b in rng f} by Th8;
then consider b such that
A1: y=r*b and
A2: b in rng f;
consider x being Element of X such that
A3: x in dom f and
A4: b=f.x by A2,PARTFUN1:3;
x in dom(r(#)f) by A3,VALUED_1:def 5;
then (r(#)f).x in rng(r(#)f) by FUNCT_1:def 3;
hence thesis by A1,A4,RFUNCT_1:57;
end;
then
A5: r**rng f c= rng(r(#)f);
for y being Element of REAL holds y in rng(r(#)f) implies y in r**rng f
proof
let y be Element of REAL;
assume y in rng(r(#)f);
then consider x being Element of X such that
A6: x in dom(r(#)f) and
A7: y=(r(#)f).x by PARTFUN1:3;
x in dom f by A6,VALUED_1:def 5;
then
A8: f.x in rng f by FUNCT_1:def 3;
reconsider fx=f.x as Real;
y = r*(fx) by A7,RFUNCT_1:57;
then y in {r*b : b in rng f} by A8;
hence thesis by Th8;
end;
then rng(r(#)f) c= r**rng f;
hence thesis by A5;
end;
theorem Th18:
for X,Z be non empty set, f be PartFunc of X,REAL holds rng(r(#)
(f|Z)) = r**rng(f|Z)
proof
let X,Z be non empty set;
let f be PartFunc of X,REAL;
for y being Element of REAL holds y in r**rng(f|Z) implies y in rng(r(#)f|Z)
proof
let y be Element of REAL;
assume y in r**rng(f|Z);
then y in {r*b : b in rng(f|Z)} by Th8;
then consider b such that
A1: y=r*b and
A2: b in rng(f|Z);
consider x being Element of X such that
A3: x in dom(f|Z) and
A4: b=(f|Z).x by A2,PARTFUN1:3;
A5: x in dom(r(#)f|Z) by A3,VALUED_1:def 5;
then y= (r(#)f|Z).x by A1,A4,VALUED_1:def 5;
hence thesis by A5,FUNCT_1:def 3;
end;
then
A6: r**rng(f|Z) c= rng(r(#)f|Z);
for y being Element of REAL holds y in rng(r(#)f|Z) implies y in r**rng(f|Z)
proof
let y be Element of REAL;
assume y in rng(r(#)f|Z);
then consider x be Element of X such that
A7: x in dom(r(#)f|Z) and
A8: y=(r(#)f|Z).x by PARTFUN1:3;
x in dom(f|Z) by A7,VALUED_1:def 5;
then
A9: (f|Z).x in rng(f|Z) by FUNCT_1:def 3;
reconsider fx = (f|Z).x as Real;
y=r*fx by A7,A8,VALUED_1:def 5;
then y in {r*b : b in rng(f|Z)} by A9;
hence thesis by Th8;
end;
then rng(r(#)f|Z) c= r**rng(f|Z);
hence thesis by A6;
end;
reserve A, B for non empty closed_interval Subset of REAL;
reserve f, g for Function of A,REAL;
reserve D, D1, D2 for Division of A;
theorem Th19:
f|A is bounded & r >= 0 implies (upper_sum_set(r(#)f)).D >= r*(
lower_bound rng f)*vol(A)
proof
assume that
A1: f|A is bounded and
A2: r >= 0;
A3: rng f is bounded_below by A1,INTEGRA1:11;
A4: (r(#)f)|A is bounded by A1,RFUNCT_1:80;
then
A5: lower_sum(r(#)f,D) >= (lower_bound rng(r(#)f))*vol(A) by INTEGRA1:25;
(upper_sum_set(r(#)f)).D = upper_sum(r(#)f,D) by INTEGRA1:def 10;
then
A6: (upper_sum_set(r(#)f)).D >= lower_sum(r(#)f,D) by A4,INTEGRA1:28;
(lower_bound rng(r(#)f))=lower_bound (r**(rng f)) by Th17
.=r*(lower_bound rng f) by A2,A3,Th15;
hence thesis by A6,A5,XXREAL_0:2;
end;
theorem Th20:
f|A is bounded & r <= 0 implies (upper_sum_set(r(#)f)).D >= r*(
upper_bound rng f)*vol(A)
proof
assume that
A1: f|A is bounded and
A2: r <= 0;
A3: rng f is bounded_above by A1,INTEGRA1:13;
A4: (r(#)f)|A is bounded by A1,RFUNCT_1:80;
then
A5: lower_sum(r(#)f,D) >= (lower_bound rng(r(#)f))*vol(A) by INTEGRA1:25;
(upper_sum_set(r(#)f)).D = upper_sum(r(#)f,D) by INTEGRA1:def 10;
then
A6: (upper_sum_set(r(#)f)).D >= lower_sum(r(#)f,D) by A4,INTEGRA1:28;
(lower_bound rng(r(#)f))=lower_bound (r**(rng f)) by Th17
.=r*(upper_bound rng f) by A2,A3,Th14;
hence thesis by A6,A5,XXREAL_0:2;
end;
theorem Th21:
f|A is bounded & r >= 0 implies (lower_sum_set(r(#)f)).D <= r*(
upper_bound rng f)*vol(A)
proof
assume that
A1: f|A is bounded and
A2: r >= 0;
A3: rng f is bounded_above by A1,INTEGRA1:13;
A4: (r(#)f)|A is bounded by A1,RFUNCT_1:80;
then
A5: upper_sum(r(#)f,D) <= (upper_bound rng(r(#)f))*vol(A) by INTEGRA1:27;
(lower_sum_set(r(#)f)).D = lower_sum(r(#)f,D) by INTEGRA1:def 11;
then
A6: (lower_sum_set(r(#)f)).D <= upper_sum(r(#)f,D) by A4,INTEGRA1:28;
(upper_bound rng(r(#)f))=upper_bound (r**(rng f)) by Th17
.=r*(upper_bound rng f) by A2,A3,Th13;
hence thesis by A6,A5,XXREAL_0:2;
end;
theorem Th22:
f|A is bounded & r <= 0 implies (lower_sum_set(r(#)f)).D <= r*(
lower_bound rng f)*vol(A)
proof
assume that
A1: f|A is bounded and
A2: r <= 0;
A3: rng f is bounded_below by A1,INTEGRA1:11;
A4: (r(#)f)|A is bounded by A1,RFUNCT_1:80;
then
A5: upper_sum(r(#)f,D) <= (upper_bound rng(r(#)f))*vol(A) by INTEGRA1:27;
(lower_sum_set(r(#)f)).D = lower_sum(r(#)f,D) by INTEGRA1:def 11;
then
A6: (lower_sum_set(r(#)f)).D <= upper_sum(r(#)f,D) by A4,INTEGRA1:28;
(upper_bound rng(r(#)f))=upper_bound (r**(rng f)) by Th17
.=r*(lower_bound rng f) by A2,A3,Th16;
hence thesis by A6,A5,XXREAL_0:2;
end;
theorem Th23:
i in dom D & f|A is bounded_above & r >= 0 implies upper_volume(
r(#)f,D).i = r*upper_volume(f,D).i
proof
assume that
A1: i in dom D and
A2: f|A is bounded_above and
A3: r >= 0;
dom(f|divset(D,i)) = dom f /\ divset(D,i) by RELAT_1:61
.= A /\ divset(D,i) by FUNCT_2:def 1
.= divset(D,i) by A1,INTEGRA1:8,XBOOLE_1:28;
then
A4: rng(f|divset(D,i)) is non empty by RELAT_1:42;
rng f is bounded_above by A2,INTEGRA1:13;
then
A5: rng(f|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43;
upper_volume(r(#)f,D).i =(upper_bound(rng((r(#)f)|divset(D,i))))*vol(
divset(D,i)) by A1,INTEGRA1:def 6
.=(upper_bound(rng(r(#)f|divset(D,i))))*vol(divset(D,i)) by RFUNCT_1:49
.=(upper_bound(r**rng(f|divset(D,i))))*vol(divset(D,i)) by Th18
.=(r*upper_bound(rng(f|divset(D,i))))*vol(divset(D,i)) by A3,A4,A5,Th13
.=r*(upper_bound(rng(f|divset(D,i)))*vol(divset(D,i)))
.=r*upper_volume(f,D).i by A1,INTEGRA1:def 6;
hence thesis;
end;
theorem Th24:
i in dom D & f|A is bounded_above & r <= 0 implies lower_volume(
r(#)f,D).i = r*upper_volume(f,D).i
proof
assume that
A1: i in dom D and
A2: f|A is bounded_above and
A3: r <= 0;
dom(f|divset(D,i)) = dom f /\ divset(D,i) by RELAT_1:61
.= A /\ divset(D,i) by FUNCT_2:def 1
.= divset(D,i) by A1,INTEGRA1:8,XBOOLE_1:28;
then
A4: rng(f|divset(D,i)) is non empty by RELAT_1:42;
rng f is bounded_above by A2,INTEGRA1:13;
then
A5: rng(f|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43;
lower_volume(r(#)f,D).i =(lower_bound(rng((r(#)f)|divset(D,i))))*vol(
divset(D,i)) by A1,INTEGRA1:def 7
.=(lower_bound(rng(r(#)f|divset(D,i))))*vol(divset(D,i)) by RFUNCT_1:49
.=(lower_bound(r**rng(f|divset(D,i))))*vol(divset(D,i)) by Th18
.=(r*upper_bound(rng(f|divset(D,i))))*vol(divset(D,i)) by A3,A4,A5,Th14
.=r*(upper_bound(rng(f|divset(D,i)))*vol(divset(D,i)))
.=r*upper_volume(f,D).i by A1,INTEGRA1:def 6;
hence thesis;
end;
theorem Th25:
i in dom D & f|A is bounded_below & r >= 0 implies lower_volume(
r(#)f,D).i = r*lower_volume(f,D).i
proof
assume that
A1: i in dom D and
A2: f|A is bounded_below and
A3: r >= 0;
dom(f|divset(D,i)) = dom f /\ divset(D,i) by RELAT_1:61
.= A /\ divset(D,i) by FUNCT_2:def 1
.= divset(D,i) by A1,INTEGRA1:8,XBOOLE_1:28;
then
A4: rng(f|divset(D,i)) is non empty by RELAT_1:42;
rng f is bounded_below by A2,INTEGRA1:11;
then
A5: rng(f|divset(D,i)) is bounded_below by RELAT_1:70,XXREAL_2:44;
lower_volume(r(#)f,D).i =(lower_bound(rng((r(#)f)|divset(D,i))))*vol(
divset(D,i)) by A1,INTEGRA1:def 7
.=(lower_bound(rng(r(#)f|divset(D,i))))*vol(divset(D,i)) by RFUNCT_1:49
.=(lower_bound(r**rng(f|divset(D,i))))*vol(divset(D,i)) by Th18
.=(r*lower_bound(rng(f|divset(D,i))))*vol(divset(D,i)) by A3,A4,A5,Th15
.=r*(lower_bound(rng(f|divset(D,i)))*vol(divset(D,i)))
.=r*lower_volume(f,D).i by A1,INTEGRA1:def 7;
hence thesis;
end;
theorem Th26:
i in dom D & f|A is bounded_below & r <= 0 implies upper_volume(
r(#)f,D).i = r*lower_volume(f,D).i
proof
assume that
A1: i in dom D and
A2: f|A is bounded_below and
A3: r <= 0;
dom(f|divset(D,i)) = dom f /\ divset(D,i) by RELAT_1:61
.= A /\ divset(D,i) by FUNCT_2:def 1
.= divset(D,i) by A1,INTEGRA1:8,XBOOLE_1:28;
then
A4: rng(f|divset(D,i)) is non empty by RELAT_1:42;
rng f is bounded_below by A2,INTEGRA1:11;
then
A5: rng(f|divset(D,i)) is bounded_below by RELAT_1:70,XXREAL_2:44;
upper_volume(r(#)f,D).i =(upper_bound(rng((r(#)f)|divset(D,i))))*vol(
divset(D,i)) by A1,INTEGRA1:def 6
.=(upper_bound(rng(r(#)f|divset(D,i))))*vol(divset(D,i)) by RFUNCT_1:49
.=(upper_bound(r**rng(f|divset(D,i))))*vol(divset(D,i)) by Th18
.=(r*lower_bound(rng(f|divset(D,i))))*vol(divset(D,i)) by A3,A4,A5,Th16
.=r*(lower_bound(rng(f|divset(D,i)))*vol(divset(D,i)))
.=r*lower_volume(f,D).i by A1,INTEGRA1:def 7;
hence thesis;
end;
theorem Th27:
f|A is bounded_above & r >= 0 implies upper_sum(r(#)f,D) = r*
upper_sum(f,D)
proof
assume
A1: f|A is bounded_above & r >= 0;
A2: for i be Nat st 1 <= i & i <= len upper_volume(r(#)f,D) holds
upper_volume(r(#)f,D).i = (r*upper_volume(f,D)).i
proof
let i be Nat;
assume
A3: 1 <= i & i <= len upper_volume(r(#)f,D);
len D = len upper_volume(r(#)f,D) by INTEGRA1:def 6;
then i in dom D by A3,FINSEQ_3:25;
then upper_volume(r(#)f,D).i = r*upper_volume(f,D).i by A1,Th23
.= (r*upper_volume(f,D)).i by RVSUM_1:44;
hence thesis;
end;
len upper_volume(r(#)f,D) = len D by INTEGRA1:def 6
.= len upper_volume(f,D) by INTEGRA1:def 6
.= len(r*upper_volume(f,D)) by NEWTON:2;
then upper_volume(r(#)f,D)=r*upper_volume(f,D) by A2,FINSEQ_1:14;
then upper_sum(r(#)f,D) =Sum(r*upper_volume(f,D)) by INTEGRA1:def 8
.=r*Sum(upper_volume(f,D)) by RVSUM_1:87
.=r*upper_sum(f,D) by INTEGRA1:def 8;
hence thesis;
end;
theorem Th28:
f|A is bounded_above & r <= 0 implies lower_sum(r(#)f,D) = r*
upper_sum(f,D)
proof
assume
A1: f|A is bounded_above & r <= 0;
A2: for i be Nat st 1 <= i & i <= len lower_volume(r(#)f,D) holds
lower_volume(r(#)f,D).i = (r*upper_volume(f,D)).i
proof
let i be Nat;
assume
A3: 1 <= i & i <= len lower_volume(r(#)f,D);
len D = len lower_volume(r(#)f,D) by INTEGRA1:def 7;
then i in dom D by A3,FINSEQ_3:25;
then lower_volume(r(#)f,D).i = r*upper_volume(f,D).i by A1,Th24
.= (r*upper_volume(f,D)).i by RVSUM_1:44;
hence thesis;
end;
len lower_volume(r(#)f,D) = len D by INTEGRA1:def 7
.= len upper_volume(f,D) by INTEGRA1:def 6
.= len(r*upper_volume(f,D)) by NEWTON:2;
then lower_volume(r(#)f,D)=r*upper_volume(f,D) by A2,FINSEQ_1:14;
then lower_sum(r(#)f,D) =Sum(r*upper_volume(f,D)) by INTEGRA1:def 9
.=r*Sum(upper_volume(f,D)) by RVSUM_1:87
.=r*upper_sum(f,D) by INTEGRA1:def 8;
hence thesis;
end;
theorem Th29:
f|A is bounded_below & r >= 0 implies lower_sum(r(#)f,D) = r*
lower_sum(f,D)
proof
assume
A1: f|A is bounded_below & r >= 0;
A2: for i be Nat st 1 <= i & i <= len lower_volume(r(#)f,D) holds
lower_volume(r(#)f,D).i = (r*lower_volume(f,D)).i
proof
let i be Nat;
assume
A3: 1 <= i & i <= len lower_volume(r(#)f,D);
len D = len lower_volume(r(#)f,D) by INTEGRA1:def 7;
then i in dom D by A3,FINSEQ_3:25;
then lower_volume(r(#)f,D).i = r*lower_volume(f,D).i by A1,Th25
.= (r*lower_volume(f,D)).i by RVSUM_1:44;
hence thesis;
end;
len lower_volume(r(#)f,D) = len D by INTEGRA1:def 7
.= len lower_volume(f,D) by INTEGRA1:def 7
.= len(r*lower_volume(f,D)) by NEWTON:2;
then lower_volume(r(#)f,D)=r*lower_volume(f,D) by A2,FINSEQ_1:14;
then lower_sum(r(#)f,D) =Sum(r*lower_volume(f,D)) by INTEGRA1:def 9
.=r*Sum(lower_volume(f,D)) by RVSUM_1:87
.=r*lower_sum(f,D) by INTEGRA1:def 9;
hence thesis;
end;
theorem Th30:
f|A is bounded_below & r <= 0 implies upper_sum(r(#)f,D) = r*
lower_sum(f,D)
proof
assume
A1: f|A is bounded_below & r <= 0;
A2: for i be Nat st 1 <= i & i <= len upper_volume(r(#)f,D) holds
upper_volume(r(#)f,D).i = (r*lower_volume(f,D)).i
proof
let i be Nat;
assume
A3: 1 <= i & i <= len upper_volume(r(#)f,D);
len D = len upper_volume(r(#)f,D) by INTEGRA1:def 6;
then i in dom D by A3,FINSEQ_3:25;
then upper_volume(r(#)f,D).i = r*lower_volume(f,D).i by A1,Th26
.= (r*lower_volume(f,D)).i by RVSUM_1:44;
hence thesis;
end;
len upper_volume(r(#)f,D) = len D by INTEGRA1:def 6
.= len lower_volume(f,D) by INTEGRA1:def 7
.= len(r*lower_volume(f,D)) by NEWTON:2;
then upper_volume(r(#)f,D)=r*lower_volume(f,D) by A2,FINSEQ_1:14;
then upper_sum(r(#)f,D) =Sum(r*lower_volume(f,D)) by INTEGRA1:def 8
.=r*Sum(lower_volume(f,D)) by RVSUM_1:87
.=r*lower_sum(f,D) by INTEGRA1:def 9;
hence thesis;
end;
theorem Th31:
f|A is bounded & f is integrable implies r(#)f is integrable &
integral(r(#)f) = r*integral(f)
proof
assume that
A1: f|A is bounded and
A2: f is integrable;
f is upper_integrable by A2,INTEGRA1:def 16;
then
A3: rng(upper_sum_set(f)) is bounded_below by INTEGRA1:def 12;
f is lower_integrable by A2,INTEGRA1:def 16;
then
A4: rng(lower_sum_set(f)) is bounded_above by INTEGRA1:def 13;
A5: now
per cases;
suppose
A6: r >= 0;
A7: for D be object st D in divs A holds (upper_sum_set(r(#)f)).D = (r(#)(
upper_sum_set(f))).D
proof
let D be object;
assume
A8: D in divs A;
then reconsider D as Division of A by INTEGRA1:def 3;
(upper_sum_set(r(#)f)).D = upper_sum(r(#) f,D) by INTEGRA1:def 10
.= r*upper_sum(f,D) by A1,A6,Th27
.= r*(upper_sum_set(f)).D by INTEGRA1:def 10
.= (r(#)(upper_sum_set(f))).D by A8,RFUNCT_1:57;
hence thesis;
end;
A9: divs A = dom(upper_sum_set(f)) by FUNCT_2:def 1
.= dom(r(#)upper_sum_set(f)) by VALUED_1:def 5;
divs A = dom upper_sum_set(r(#)f) by FUNCT_2:def 1;
then upper_sum_set(r(#)f) = r(#)upper_sum_set(f) by A9,A7,FUNCT_1:2;
then
A10: upper_integral(r(#)f) = lower_bound rng(r(#) upper_sum_set(f)) by
INTEGRA1:def 14
.= lower_bound(r**(rng(upper_sum_set(f)))) by Th17
.= r*lower_bound(rng(upper_sum_set(f))) by A3,A6,Th15
.= r*upper_integral(f) by INTEGRA1:def 14;
A11: for D be object st D in divs A holds (lower_sum_set(r(#)f)).D = (r(#)(
lower_sum_set(f))).D
proof
let D be object;
assume
A12: D in divs A;
then reconsider D as Division of A by INTEGRA1:def 3;
(lower_sum_set(r(#)f)).D = lower_sum(r(#) f,D) by INTEGRA1:def 11
.= r*lower_sum(f,D) by A1,A6,Th29
.= r*(lower_sum_set(f)).D by INTEGRA1:def 11
.= (r(#)(lower_sum_set(f))).D by A12,RFUNCT_1:57;
hence thesis;
end;
A13: divs A = dom(lower_sum_set(f)) by FUNCT_2:def 1
.= dom(r(#)lower_sum_set(f)) by VALUED_1:def 5;
divs A = dom lower_sum_set(r(#)f) by FUNCT_2:def 1;
then lower_sum_set(r(#)f) = r(#)lower_sum_set(f) by A13,A11,FUNCT_1:2;
then lower_integral(r(#)f) = upper_bound rng(r(#) lower_sum_set(f)) by
INTEGRA1:def 15
.= upper_bound(r**(rng(lower_sum_set(f)))) by Th17
.= r*upper_bound(rng(lower_sum_set(f))) by A4,A6,Th13
.= r*lower_integral(f) by INTEGRA1:def 15
.= r*upper_integral(f) by A2,INTEGRA1:def 16;
hence upper_integral(r(#)f) = lower_integral(r(#)f) by A10;
thus upper_integral(r(#)f) = r*integral(f) by A10,INTEGRA1:def 17;
end;
suppose
A14: r < 0;
A15: for D be object st D in divs A holds (upper_sum_set(r(#)f)).D = (r(#)(
lower_sum_set(f))).D
proof
let D be object;
assume
A16: D in divs A;
then reconsider D as Division of A by INTEGRA1:def 3;
(upper_sum_set(r(#)f)).D=upper_sum(r(#)f,D) by INTEGRA1:def 10
.= r*lower_sum(f,D) by A1,A14,Th30
.= r*(lower_sum_set(f)).D by INTEGRA1:def 11
.= (r(#)(lower_sum_set(f))).D by A16,RFUNCT_1:57;
hence thesis;
end;
A17: divs A = dom(lower_sum_set(f)) by FUNCT_2:def 1
.= dom(r(#)lower_sum_set(f)) by VALUED_1:def 5;
divs A = dom upper_sum_set(r(#)f) by FUNCT_2:def 1;
then upper_sum_set(r(#)f) = r(#)lower_sum_set(f) by A17,A15,FUNCT_1:2;
then
A18: upper_integral(r(#)f) = lower_bound rng(r(#) lower_sum_set(f)) by
INTEGRA1:def 14
.= lower_bound(r**(rng(lower_sum_set(f)))) by Th17
.= r*upper_bound(rng(lower_sum_set(f))) by A4,A14,Th14
.= r*lower_integral(f) by INTEGRA1:def 15;
A19: for D be object st D in divs A holds (lower_sum_set(r(#)f)).D = (r(#)(
upper_sum_set(f))).D
proof
let D be object;
assume
A20: D in divs A;
then reconsider D as Division of A by INTEGRA1:def 3;
(lower_sum_set(r(#)f)).D=lower_sum(r(#)f,D) by INTEGRA1:def 11
.= r*upper_sum(f,D) by A1,A14,Th28
.= r*(upper_sum_set(f)).D by INTEGRA1:def 10
.= (r(#)(upper_sum_set(f))).D by A20,RFUNCT_1:57;
hence thesis;
end;
A21: divs A = dom(upper_sum_set(f)) by FUNCT_2:def 1
.= dom(r(#)upper_sum_set(f)) by VALUED_1:def 5;
divs A = dom lower_sum_set(r(#)f) by FUNCT_2:def 1;
then lower_sum_set(r(#)f) = r(#)upper_sum_set(f) by A21,A19,FUNCT_1:2;
then lower_integral(r(#)f) = upper_bound rng(r(#) upper_sum_set(f)) by
INTEGRA1:def 15
.= upper_bound(r**(rng(upper_sum_set(f)))) by Th17
.= r*lower_bound(rng(upper_sum_set(f))) by A3,A14,Th16
.= r*upper_integral(f) by INTEGRA1:def 14
.= r*lower_integral(f) by A2,INTEGRA1:def 16;
hence upper_integral(r(#)f) = lower_integral(r(#)f) by A18;
upper_integral(r(#)f) = r*upper_integral(f) by A2,A18,INTEGRA1:def 16
.= r*integral(f) by INTEGRA1:def 17;
hence upper_integral(r(#)f) = r*integral(f);
end;
end;
ex a st for D be object st D in divs A /\ dom(lower_sum_set(r(#)f)) holds
a >= (lower_sum_set(r(#)f)).D
proof
now
per cases;
suppose
A22: r>=0;
for D be object st D in divs A /\ dom(lower_sum_set(r(#)f)) holds r*
(upper_bound rng f)*vol(A) >= (lower_sum_set(r(#)f)).D
proof
let D be object;
assume D in divs A /\ dom(lower_sum_set(r(#)f));
then D is Division of A by INTEGRA1:def 3;
hence thesis by A1,A22,Th21;
end;
hence thesis;
end;
suppose
A23: r<0;
for D be object st D in divs A /\ dom(lower_sum_set(r(#)f)) holds r*
(lower_bound rng f)*vol(A) >= (lower_sum_set(r(#)f)).D
proof
let D be object;
assume D in divs A /\ dom(lower_sum_set(r(#)f));
then D is Division of A by INTEGRA1:def 3;
hence thesis by A1,A23,Th22;
end;
hence thesis;
end;
end;
hence thesis;
end;
then (lower_sum_set(r(#)f))|divs A is bounded_above by RFUNCT_1:70;
then rng lower_sum_set(r(#)f) is bounded_above by INTEGRA1:13;
then
A24: r(#)f is lower_integrable by INTEGRA1:def 13;
ex a st for D be object st D in divs A /\ dom(upper_sum_set(r(#)f)) holds a
<= (upper_sum_set(r(#)f)).D
proof
now
per cases;
suppose
A25: r>=0;
for D be object st D in divs A /\ dom(upper_sum_set(r(#)f)) holds r*(
lower_bound rng f)*vol(A) <= (upper_sum_set(r(#)f)).D
proof
let D be object;
assume D in divs A /\ dom(upper_sum_set(r(#)f));
then D is Division of A by INTEGRA1:def 3;
hence thesis by A1,A25,Th19;
end;
hence thesis;
end;
suppose
A26: r<0;
for D be object st D in divs A /\ dom(upper_sum_set(r(#)f)) holds r*
(upper_bound rng f)*vol(A) <= (upper_sum_set(r(#)f)).D
proof
let D be object;
assume D in divs A /\ dom(upper_sum_set(r(#)f));
then D is Division of A by INTEGRA1:def 3;
hence thesis by A1,A26,Th20;
end;
hence thesis;
end;
end;
hence thesis;
end;
then (upper_sum_set(r(#)f))|divs A is bounded_below by RFUNCT_1:71;
then rng upper_sum_set(r(#)f) is bounded_below by INTEGRA1:11;
then r(#)f is upper_integrable by INTEGRA1:def 12;
hence thesis by A24,A5,INTEGRA1:def 16,def 17;
end;
begin :: Monotonicity of Integral
theorem Th32:
f|A is bounded & (for x st x in A holds f.x >= 0) implies
integral(f) >= 0
proof
assume that
A1: f|A is bounded and
A2: for x st x in A holds f.x >= 0;
A3: for a be Real st a in rng upper_sum_set(f) holds a >= 0
proof
let a be Real;
assume a in rng upper_sum_set(f);
then consider D being Element of divs A such that
A4: D in dom upper_sum_set(f) & a=(upper_sum_set(f)).D by PARTFUN1:3;
reconsider D as Division of A by INTEGRA1:def 3;
A5: for i be Nat st i in dom upper_volume(f,D) holds 0 <= upper_volume(f,D
). i
proof
let i be Nat;
set r = upper_volume(f,D).i;
assume
A6: i in dom upper_volume(f,D);
len D = len upper_volume(f,D) by INTEGRA1:def 6;
then
A7: i in dom D by A6,FINSEQ_3:29;
A8: upper_bound (rng(f|divset(D,i))) >= 0
proof
rng f is bounded_above by A1,INTEGRA1:13;
then
A9: rng(f|divset(D,i)) is bounded_above by RELAT_1:70,XXREAL_2:43;
dom(f|divset(D,i)) = dom f /\ divset(D,i) & dom f = A by FUNCT_2:def 1
,RELAT_1:61;
then dom(f|divset(D,i)) is non empty Subset of REAL by A7,INTEGRA1:8
,XBOOLE_1:28;
then consider x being Element of REAL such that
A10: x in dom(f|divset(D,i)) by SUBSET_1:4;
f.x >= 0 by A2,A10;
then
A11: (f|divset(D,i)).x >= 0 by A10,FUNCT_1:47;
(f|divset(D,i)).x in rng(f|divset(D,i)) by A10,FUNCT_1:def 3;
hence thesis by A9,A11,SEQ_4:def 1;
end;
A12: vol(divset(D,i)) >= 0 by INTEGRA1:9;
r = (upper_bound (rng (f|divset(D,i))))*vol(divset(D,i)) by A7,
INTEGRA1:def 6;
hence thesis by A12,A8;
end;
a = upper_sum(f,D) by A4,INTEGRA1:def 10
.= Sum(upper_volume(f,D)) by INTEGRA1:def 8;
hence thesis by A5,RVSUM_1:84;
end;
upper_integral(f) = lower_bound rng upper_sum_set(f) & rng upper_sum_set
(f) is non empty by INTEGRA1:def 14;
then upper_integral(f) >= 0 by A3,SEQ_4:43;
hence thesis by INTEGRA1:def 17;
end;
theorem Th33:
f|A is bounded & f is integrable & g|A is bounded & g is
integrable implies f-g is integrable & integral(f-g) = integral(f)-integral(g)
proof
assume that
A1: f|A is bounded & f is integrable and
A2: g|A is bounded and
A3: g is integrable;
A4: -g is integrable by A2,A3,Th31;
A5: (-g)|A is bounded by A2,RFUNCT_1:82;
hence f-g is integrable by A1,A4,INTEGRA1:57;
integral(-g) = (-1)*integral(g) by A2,A3,Th31;
then integral(f-g)=integral(f)+-integral(g) by A1,A5,A4,INTEGRA1:57;
hence thesis;
end;
theorem
f|A is bounded & f is integrable & g|A is bounded & g is integrable &
(for x st x in A holds f.x >= g.x) implies integral(f) >= integral(g)
proof
assume that
A1: f|A is bounded & f is integrable & g|A is bounded & g is integrable and
A2: for x st x in A holds f.x >= g.x;
A3: dom (f-g)= A by FUNCT_2:def 1;
A4: for x st x in A holds (f-g).x >= 0
proof
let x;
assume
A5: x in A;
then (f-g).x = f.x - g.x by A3,VALUED_1:13;
hence thesis by A2,A5,XREAL_1:48;
end;
integral(f-g)=integral(f)-integral(g) & (f-g)|(A /\ A) is bounded by A1,Th33,
RFUNCT_1:84;
hence thesis by A4,Th32,XREAL_1:49;
end;
begin :: Definition of Division Sequence
theorem
f|A is bounded implies rng upper_sum_set(f) is bounded_below
proof
set D1 = the Division of A;
assume
A1: f|A is bounded;
take lower_sum(f,D1);
let a be ExtReal;
assume a in rng upper_sum_set(f);
then consider D be Element of divs A such that
A2: D in dom upper_sum_set(f) & a = (upper_sum_set(f)).D by PARTFUN1:3;
reconsider D as Division of A by INTEGRA1:def 3;
a = upper_sum(f,D) by A2,INTEGRA1:def 10;
hence thesis by A1,INTEGRA1:48;
end;
theorem
f|A is bounded implies rng lower_sum_set(f) is bounded_above
proof
set D1 = the Division of A;
assume
A1: f|A is bounded;
take upper_sum(f,D1);
let a be ExtReal;
assume a in rng lower_sum_set(f);
then consider D be Element of divs A such that
A2: D in dom lower_sum_set(f) & a = (lower_sum_set(f)).D by PARTFUN1:3;
reconsider D as Division of A by INTEGRA1:def 3;
a = lower_sum(f,D) by A2,INTEGRA1:def 11;
hence thesis by A1,INTEGRA1:48;
end;
definition
let A be non empty closed_interval Subset of REAL;
mode DivSequence of A is sequence of divs A;
end;
definition
let A;
let T be DivSequence of A;
let i;
redefine func T.i -> Division of A; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider i as Element of NAT by ORDINAL1:def 12;
T.i is Element of divs A;
hence thesis by INTEGRA1:def 3;
end;
end;
definition
let A be non empty closed_interval Subset of REAL, f be PartFunc of A,REAL,
T be DivSequence of A;
func upper_sum(f,T) -> Real_Sequence means
for i holds it.i = upper_sum(f,T.i);
existence
proof
deffunc F(Nat)=upper_sum(f,T.In($1,NAT));
consider IT being Real_Sequence such that
A1: for i being Nat holds IT.i = F(i) from SEQ_1:sch 1;
take IT;
let i;
IT.i = F(i) by A1;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Real_Sequence such that
A2: for i holds F1.i = upper_sum(f,T.i) and
A3: for i holds F2.i = upper_sum(f,T.i);
for i being Element of NAT holds F1.i = F2.i
proof
let i be Element of NAT;
F1.i = upper_sum(f,T.i) by A2
.= F2.i by A3;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
func lower_sum(f,T) -> Real_Sequence means
for i holds it.i = lower_sum(f,T.
i);
existence
proof
deffunc F(Nat)=lower_sum(f,T.In($1,NAT));
consider IT being Real_Sequence such that
A4: for i being Nat holds IT.i = F(i)
from SEQ_1:sch 1;
take IT;
let i;
IT.i = F(i) by A4;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Real_Sequence such that
A5: for i holds F1.i = lower_sum(f,T.i) and
A6: for i holds F2.i = lower_sum(f,T.i);
for i being Element of NAT holds F1.i = F2.i
proof
let i be Element of NAT;
F1.i = lower_sum(f,T.i) by A5
.= F2.i by A6;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
end;
theorem
D1 <= D2 implies for j st j in dom D2 holds ex i st i in dom D1
& divset(D2,j) c= divset(D1,i)
proof
assume
A1: D1 <= D2;
let j;
defpred P[set] means D2.$1 in rng D1 & D2.$1 >= D2.j;
consider X being Subset of dom D2 such that
A2: for x1 holds x1 in X iff x1 in dom D2 & P[x1] from SUBSET_1:sch 1;
reconsider X as Subset of NAT by XBOOLE_1:1;
assume
A3: j in dom D2;
ex n st n in dom D2 & D2.n in rng D1 & D2.n >= D2.j
proof
take len D2;
len D2 in Seg len D2 by FINSEQ_1:3;
then
A4: len D2 in dom D2 by FINSEQ_1:def 3;
len D1 in Seg len D1 by FINSEQ_1:3;
then
A5: len D1 in dom D1 by FINSEQ_1:def 3;
D2.(len D2) = upper_bound A by INTEGRA1:def 2;
then
A6: D1.(len D1) = D2.(len D2) by INTEGRA1:def 2;
j in Seg len D2 by A3,FINSEQ_1:def 3;
then j <= len D2 by FINSEQ_1:1;
hence thesis by A3,A5,A6,A4,FUNCT_1:def 3,SEQ_4:137;
end;
then reconsider X as non empty Subset of NAT by A2;
A7: min X in X by XXREAL_2:def 7;
then
A8: D2.(min X) >= D2.j by A2;
D2.(min X) in rng D1 by A2,A7;
then consider i being Element of NAT such that
A9: i in dom D1 and
A10: D2.(min X)=D1.i by PARTFUN1:3;
take i;
A11: D1.i >= D2.j by A2,A7,A10;
divset(D2,j) c= divset(D1,i)
proof
now
per cases;
suppose
i=1;
then
lower_bound divset(D1,i) = lower_bound A & upper_bound divset(D1,
i) = D1.i by A9,INTEGRA1:def 4;
then
A12: divset(D1,i) = [.lower_bound A,D1.i .] by INTEGRA1:4;
now
per cases;
suppose
A13: j=1;
D1.i in rng D1 & rng D1 c= A by A9,FUNCT_1:def 3,INTEGRA1:def 2;
then
A14: D1.i in A;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4;
then D1.i in {r:lower_bound A<=r & r<=upper_bound A} by A14,
RCOMP_1:def 1;
then ex x st x=D1.i & lower_bound A<=x & x<=upper_bound A;
then lower_bound A in {r:lower_bound A <= r & r <= D1.i};
then
A15: lower_bound A in [.lower_bound A,D1.i .] by RCOMP_1:def 1;
D2.j in rng D2 & rng D2 c= A by A3,FUNCT_1:def 3,INTEGRA1:def 2;
then
A16: D2.j in A;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4;
then D2.j in {r:lower_bound A<=r & r<=upper_bound A} by A16,
RCOMP_1:def 1;
then ex x st x=D2.j & lower_bound A<=x & x<=upper_bound A;
then D2.j in {r:lower_bound A <= r & r <= D1.i} by A8,A10;
then
A17: D2.j in [.lower_bound A,D1.i .] by RCOMP_1:def 1;
lower_bound divset(D2,j) = lower_bound A & upper_bound divset
(D2,j) = D2.j by A3,A13,INTEGRA1:def 4;
then divset(D2,j) = [.lower_bound A,D2.j .] by INTEGRA1:4;
hence thesis by A12,A15,A17,XXREAL_2:def 12;
end;
suppose
A18: j<>1;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4;
then
A19: A = {r:lower_bound A<=r & r<=upper_bound A} by RCOMP_1:def 1;
D2.j in rng D2 & rng D2 c= A by A3,FUNCT_1:def 3,INTEGRA1:def 2;
then D2.j in {r:lower_bound A<=r & r<=upper_bound A} by A19;
then ex x st x=D2.j & lower_bound A <= x & x <= upper_bound A;
then D2.j in {r:lower_bound A <= r & r <= D1.i} by A8,A10;
then
A20: D2.j in [.lower_bound A,D1.i .] by RCOMP_1:def 1;
A = [.lower_bound A,upper_bound A.] by INTEGRA1:4;
then
A21: A = {r:lower_bound A<=r & r<=upper_bound A} by RCOMP_1:def 1;
A22: rng D2 c= A by INTEGRA1:def 2;
A23: j-1 in dom D2 by A3,A18,INTEGRA1:7;
then D2.(j-1) in rng D2 by FUNCT_1:def 3;
then D2.(j-1) in {r:lower_bound A<=r & r<=upper_bound A} by A21,A22
;
then
A24: ex x st x=D2.(j-1) & lower_bound A <= x & x <= upper_bound A;
j <= j+1 by NAT_1:11;
then j-1 <= j by XREAL_1:20;
then D2.(j-1) <= D2.j by A3,A23,SEQ_4:137;
then D2.(j-1) <= D1.i by A8,A10,XXREAL_0:2;
then D2.(j-1) in {r:lower_bound A <= r & r <= D1.i} by A24;
then
A25: D2.(j-1) in [.lower_bound A,D1.i .] by RCOMP_1:def 1;
lower_bound divset(D2,j) = D2.(j-1) & upper_bound divset(D2,j
) = D2.j by A3,A18,INTEGRA1:def 4;
then divset(D2,j) = [. D2.(j-1),D2.j .] by INTEGRA1:4;
hence thesis by A12,A25,A20,XXREAL_2:def 12;
end;
end;
hence thesis;
end;
suppose
A26: i<>1;
A27: j <> 1
proof
assume
A28: j=1;
A29: i in Seg len D1 by A9,FINSEQ_1:def 3;
then
A30: 1 <= i by FINSEQ_1:1;
i <= len D1 by A29,FINSEQ_1:1;
then 1 <= len D1 by A30,XXREAL_0:2;
then 1 in Seg len D1 by FINSEQ_1:1;
then
A31: 1 in dom D1 by FINSEQ_1:def 3;
then
A32: D1.1 in rng D1 by FUNCT_1:def 3;
rng D1 c= rng D2 by A1,INTEGRA1:def 18;
then consider n being Element of NAT such that
A33: n in dom D2 and
A34: D1.1 = D2.n by A32,PARTFUN1:3;
A35: n in Seg len D2 by A33,FINSEQ_1:def 3;
then
A36: 1 <= n by FINSEQ_1:1;
n <= len D2 by A35,FINSEQ_1:1;
then 1 <= len D2 by A36,XXREAL_0:2;
then 1 in Seg len D2 by FINSEQ_1:1;
then 1 in dom D2 by FINSEQ_1:def 3;
then D2.j <= D2.n by A28,A33,A36,SEQ_4:137;
then n in X by A2,A32,A33,A34;
then n >= min X by XXREAL_2:def 7;
then
A37: D1.1 >= D1.i by A7,A10,A33,A34,SEQ_4:137;
i > 1 by A26,A30,XXREAL_0:1;
hence contradiction by A9,A31,A37,SEQM_3:def 1;
end;
then
A38: j-1 in dom D2 by A3,INTEGRA1:7;
A39: D1.(i-1) <= D2.(j-1)
proof
A40: i-1 in dom D1 by A9,A26,INTEGRA1:7;
then
A41: D1.(i-1) in rng D1 by FUNCT_1:def 3;
rng D1 c= rng D2 by A1,INTEGRA1:def 18;
then consider n being Element of NAT such that
A42: n in dom D2 & D1.(i-1) = D2.n by A41,PARTFUN1:3;
assume D1.(i-1) > D2.(j-1);
then n > j-1 by A38,A42,SEQ_4:137;
then n+1 > j by XREAL_1:19;
then n >= j by NAT_1:13;
then D1.(i-1) >= D2.j by A3,A42,SEQ_4:137;
then n in X by A2,A41,A42;
then n >= min X by XXREAL_2:def 7;
then D1.(i-1) >= D1.i by A7,A10,A42,SEQ_4:137;
then i-1 >= i by A9,A40,SEQM_3:def 1;
then
A43: i >= i+1 by XREAL_1:19;
i <= i+1 by NAT_1:11;
then i = i+1 by A43,XXREAL_0:1;
hence contradiction;
end;
j <= j+1 by NAT_1:11;
then j-1 <= j by XREAL_1:20;
then
A44: D2.(j-1) <= D2.j by A3,A38,SEQ_4:137;
then
A45: D1.(i-1) <= D2.j by A39,XXREAL_0:2;
D2.(j-1) <= D1.i by A11,A44,XXREAL_0:2;
then D2.(j-1) in {r:D1.(i-1)<=r & r<=D1.i} by A39;
then
A46: D2.(j-1) in [. D1.(i-1),D1.i .] by RCOMP_1:def 1;
D2.j <= D1.i by A2,A7,A10;
then D2.j in {r:D1.(i-1) <= r & r <= D1.i} by A45;
then
A47: D2.j in [. D1.(i-1),D1.i .] by RCOMP_1:def 1;
lower_bound divset(D2,j) = D2.(j-1) & upper_bound divset(D2,j) =
D2.j by A3,A27,INTEGRA1:def 4;
then
A48: divset(D2,j) = [. D2.(j-1),D2.j .] by INTEGRA1:4;
lower_bound divset(D1,i) = D1.(i-1) & upper_bound divset(D1,i) =
D1.i by A9,A26,INTEGRA1:def 4;
then divset(D1,i) = [. D1.(i-1),D1.i .] by INTEGRA1:4;
hence thesis by A48,A46,A47,XXREAL_2:def 12;
end;
end;
hence thesis;
end;
hence thesis by A9;
end;
theorem
A c= B implies vol(A) <= vol(B)
proof
assume
A1: A c= B;
vol(A) = upper_bound A - lower_bound A by INTEGRA1:def 5;
then upper_bound B >= vol(A) + lower_bound A by A1,SEQ_4:48;
then
A2: upper_bound B - vol(A) >= lower_bound A by XREAL_1:19;
lower_bound A >= lower_bound B by A1,SEQ_4:47;
then upper_bound B - vol(A) >= lower_bound B by A2,XXREAL_0:2;
then upper_bound B - lower_bound B >= vol(A) by XREAL_1:11;
hence thesis by INTEGRA1:def 5;
end;
theorem
for A being Subset of REAL,
a,x being Real st x in a ** A holds
ex b being Real st b in A & x = a * b
proof
let A be Subset of REAL,
a,x be Real;
assume x in a ** A; then
x in {a*b where b is Element of ExtREAL : b in A} by MEMBER_1:187; then
consider b being Element of ExtREAL such that
A1: x = a*b & b in A;
reconsider b as Real by A1;
take b;
x = a*b by A1,XXREAL_3:def 5;
hence thesis by A1;
end;
begin :: Addenda
:: missing, 2008.06.10
theorem
for A being non empty ext-real-membered set holds 0 ** A = {0}
proof
let A be non empty ext-real-membered set;
for e being object holds e in 0**A iff e = 0
proof
let e be object;
consider r being ExtReal such that
A1: r in A by MEMBERED:8;
hereby
assume e in 0**A;
then ex z being Element of ExtREAL st e = 0 * z & z in A
by MEMBER_1:188;
hence e = 0;
end;
assume e = 0;
then e = 0*r;
hence thesis by A1,MEMBER_1:186;
end;
hence thesis by TARSKI:def 1;
end;