:: INTEGRA2 semantic presentation begin theorem :: INTEGRA2:1 for A being non empty closed_interval Subset of REAL for x being real number holds ( x in A iff ( lower_bound A <= x & x <= upper_bound A ) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for x being real number holds ( x in A iff ( lower_bound A <= x & x <= upper_bound A ) ) let x be real number ; ::_thesis: ( x in A iff ( lower_bound A <= x & x <= upper_bound A ) ) hereby ::_thesis: ( lower_bound A <= x & x <= upper_bound A implies x in A ) assume x in A ; ::_thesis: ( lower_bound A <= x & x <= upper_bound A ) then x in [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then x in { a where a is Real : ( lower_bound A <= a & a <= upper_bound A ) } by RCOMP_1:def_1; then ex a being Real st ( a = x & lower_bound A <= a & a <= upper_bound A ) ; hence ( lower_bound A <= x & x <= upper_bound A ) ; ::_thesis: verum end; assume A1: ( lower_bound A <= x & x <= upper_bound A ) ; ::_thesis: x in A x is Real by XREAL_0:def_1; then x in { a where a is Real : ( 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 x in A by INTEGRA1:4; ::_thesis: verum end; definition let IT be FinSequence of REAL ; attrIT is non-decreasing means :Def1: :: INTEGRA2:def 1 for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n <= IT . (n + 1); end; :: deftheorem Def1 defines non-decreasing INTEGRA2:def_1_:_ for IT being FinSequence of REAL holds ( IT is non-decreasing iff for n being Element of NAT st n in dom IT & n + 1 in dom IT holds IT . n <= IT . (n + 1) ); registration cluster Relation-like NAT -defined REAL -valued Function-like V34() V35() V36() V51() FinSequence-like FinSubsequence-like non-decreasing for FinSequence of REAL ; existence ex b1 being FinSequence of REAL st b1 is non-decreasing proof take f = <*> REAL; ::_thesis: f is non-decreasing let n be Element of NAT ; :: according to INTEGRA2:def_1 ::_thesis: ( n in dom f & n + 1 in dom f implies f . n <= f . (n + 1) ) assume that A1: n in dom f and n + 1 in dom f ; ::_thesis: f . n <= f . (n + 1) thus f . n <= f . (n + 1) by A1; ::_thesis: verum end; end; theorem :: INTEGRA2:2 for p being non-decreasing FinSequence of REAL for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds p . i <= p . j proof let p be non-decreasing FinSequence of REAL ; ::_thesis: for i, j being Element of NAT st i in dom p & j in dom p & i <= j holds p . i <= p . j let i, j be Element of NAT ; ::_thesis: ( i in dom p & j in dom p & i <= j implies p . i <= p . j ) assume A1: i in dom p ; ::_thesis: ( not j in dom p or not i <= j or p . i <= p . j ) defpred S1[ Element of NAT ] means for i, j being Element of NAT st j = i + \$1 & i in dom p & j in dom p holds p . i <= p . j; assume A2: j in dom p ; ::_thesis: ( not i <= j or p . i <= p . j ) A3: 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] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] S1[k + 1] proof let i, j be Element of NAT ; ::_thesis: ( j = i + (k + 1) & i in dom p & j in dom p implies p . i <= p . j ) reconsider l = i + k as Element of NAT ; A5: 0 <= k by NAT_1:2; assume j = i + (k + 1) ; ::_thesis: ( not i in dom p or not j in dom p or p . i <= p . j ) then A6: j = l + 1 ; assume A7: i in dom p ; ::_thesis: ( not j in dom p or p . i <= p . j ) then 1 <= i by FINSEQ_3:25; then A8: 1 + 0 <= l by A5, XREAL_1:7; assume A9: j in dom p ; ::_thesis: p . i <= p . j then j <= len p by FINSEQ_3:25; then l < len p by A6, NAT_1:13; then A10: l in dom p by A8, FINSEQ_3:25; then A11: p . i <= p . l by A4, A7; p . l <= p . j by A9, A6, A10, Def1; hence p . i <= p . j by A11, XXREAL_0:2; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A12: S1[ 0 ] ; A13: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A12, A3); assume i <= j ; ::_thesis: p . i <= p . j then consider n being Nat such that A14: j = i + n by NAT_1:10; reconsider n = n as Element of NAT by ORDINAL1:def_12; j = i + n by A14; hence p . i <= p . j by A1, A2, A13; ::_thesis: verum end; theorem :: INTEGRA2:3 for p being FinSequence of REAL ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent proof let p be FinSequence of REAL ; ::_thesis: ex q being non-decreasing FinSequence of REAL st p,q are_fiberwise_equipotent consider q being non-increasing FinSequence of REAL such that A1: p,q are_fiberwise_equipotent by RFINSEQ:22; for n being Element of NAT st n in dom (Rev q) & n + 1 in dom (Rev q) holds (Rev q) . n <= (Rev q) . (n + 1) proof let n be Element of NAT ; ::_thesis: ( n in dom (Rev q) & n + 1 in dom (Rev q) implies (Rev q) . n <= (Rev q) . (n + 1) ) assume that A2: n in dom (Rev q) and A3: n + 1 in dom (Rev q) ; ::_thesis: (Rev q) . n <= (Rev q) . (n + 1) (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 = m as Element of NAT by ORDINAL1:def_12; ( 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; set 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; ( (Rev q) . n = q . (((len q) - n) + 1) & (Rev q) . (n + 1) = q . (((len q) - (n + 1)) + 1) ) by A2, A3, FINSEQ_5:def_3; hence (Rev q) . n <= (Rev q) . (n + 1) by A6, A9, RFINSEQ:def_3; ::_thesis: verum end; hence (Rev q) . n <= (Rev q) . (n + 1) ; ::_thesis: verum end; then reconsider r = Rev q as non-decreasing FinSequence of REAL by Def1; take r ; ::_thesis: p,r are_fiberwise_equipotent p, Rev q are_fiberwise_equipotent proof defpred S1[ Element of NAT ] means for p being FinSequence of REAL for q being non-increasing FinSequence of REAL st len p = \$1 & p,q are_fiberwise_equipotent holds p, Rev q are_fiberwise_equipotent ; 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] ) assume A11: S1[k] ; ::_thesis: S1[k + 1] S1[k + 1] proof let p be FinSequence of REAL ; ::_thesis: for q being non-increasing FinSequence of REAL st len p = k + 1 & p,q are_fiberwise_equipotent holds p, Rev q are_fiberwise_equipotent let q be non-increasing FinSequence of REAL ; ::_thesis: ( len p = k + 1 & p,q are_fiberwise_equipotent implies p, Rev q are_fiberwise_equipotent ) consider q1 being non-increasing FinSequence of REAL such that A12: p,q1 are_fiberwise_equipotent by RFINSEQ:22; reconsider q1k = q1 | k 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 ; ::_thesis: ( not p,q are_fiberwise_equipotent or p, Rev q are_fiberwise_equipotent ) 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 ; ::_thesis: p, Rev q are_fiberwise_equipotent then q = q1 by A12, CLASSES1:76, RFINSEQ:23; hence p, Rev q are_fiberwise_equipotent by A12, A16, A17, CLASSES1:76; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A18: len p = len p ; A19: S1[ 0 ] proof let p be FinSequence of REAL ; ::_thesis: for q being non-increasing FinSequence of REAL st len p = 0 & p,q are_fiberwise_equipotent holds p, Rev q are_fiberwise_equipotent let q be non-increasing FinSequence of REAL ; ::_thesis: ( len p = 0 & p,q are_fiberwise_equipotent implies p, Rev q are_fiberwise_equipotent ) assume A20: len p = 0 ; ::_thesis: ( not p,q are_fiberwise_equipotent or p, Rev q are_fiberwise_equipotent ) assume p,q are_fiberwise_equipotent ; ::_thesis: p, Rev 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 being set holds card (Coim (p,x)) = card (Coim ((Rev q),x)) proof let x be set ; ::_thesis: card (Coim (p,x)) = card (Coim ((Rev q),x)) card (p " {x}) = 0 by A22, CARD_1:27, FUNCT_1:72; hence card (Coim (p,x)) = card (Coim ((Rev q),x)) by A21, CARD_1:27, FUNCT_1:72; ::_thesis: verum end; hence p, Rev q are_fiberwise_equipotent by CLASSES1:def_9; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A19, A10); hence p, Rev q are_fiberwise_equipotent by A1, A18; ::_thesis: verum end; hence p,r are_fiberwise_equipotent ; ::_thesis: verum end; theorem :: INTEGRA2:4 for D being non empty set for f being FinSequence of D for k1, k2, k3 being Element of 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 ; ::_thesis: for f being FinSequence of D for k1, k2, k3 being Element of 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) let f be FinSequence of D; ::_thesis: for k1, k2, k3 being Element of 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) let k1, k2, k3 be Element of NAT ; ::_thesis: ( 1 <= k1 & k3 <= len f & k1 <= k2 & k2 < k3 implies (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3) ) assume that A1: 1 <= k1 and A2: k3 <= len f and A3: k1 <= k2 and A4: k2 < k3 ; ::_thesis: (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,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 being 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; ::_thesis: ( 1 <= k & k <= len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) implies ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k ) assume A17: ( 1 <= k & k <= len ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) ) ; ::_thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k 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__::_thesis:_((mid_(f,k1,k2))_^_(mid_(f,(k2_+_1),k3)))_._k_=_(mid_(f,k1,k3))_._k percases ( k in dom (mid (f,k1,k2)) or ex n being Nat st ( n in dom (mid (f,(k2 + 1),k3)) & k = (len (mid (f,k1,k2))) + n ) ) by A18, FINSEQ_1:25; supposeA19: k in dom (mid (f,k1,k2)) ; ::_thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k 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, A19, A21, A22, FINSEQ_6:122 ; hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k by A1, A2, A10, A19, A21, A23, FINSEQ_6:122; ::_thesis: verum end; suppose ex n being Nat st ( n in dom (mid (f,(k2 + 1),k3)) & k = (len (mid (f,k1,k2))) + n ) ; ::_thesis: ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k then consider n being 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, A24, A27, FINSEQ_6:122 .= f . ((n + k2) + 0) ; hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k by A26; ::_thesis: verum end; end; end; hence ((mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3))) . k = (mid (f,k1,k3)) . k ; ::_thesis: verum 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 (mid (f,k1,k2)) ^ (mid (f,(k2 + 1),k3)) = mid (f,k1,k3) by A14, A16, FINSEQ_1:14; ::_thesis: verum end; begin definition let A be real-membered set ; let x be real number ; :: original: ** redefine funcx ** A -> Subset of REAL; coherence x ** A is Subset of REAL by MEMBERED:3; end; theorem :: INTEGRA2:5 for X, Y being non empty set for f being 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 ; ::_thesis: for f being PartFunc of X,REAL st f | X is bounded_above & Y c= X holds (f | Y) | Y is bounded_above let f be PartFunc of X,REAL; ::_thesis: ( f | X is bounded_above & Y c= X implies (f | Y) | Y is bounded_above ) assume f | X is bounded_above ; ::_thesis: ( not Y c= X or (f | Y) | Y is bounded_above ) then consider a being real number such that A1: for x being set st x in X /\ (dom f) holds a >= f . x by RFUNCT_1:70; assume A2: Y c= X ; ::_thesis: (f | Y) | Y is bounded_above for x being set st x in Y /\ (dom (f | Y)) holds a >= (f | Y) . x proof let x be set ; ::_thesis: ( x in Y /\ (dom (f | Y)) implies a >= (f | Y) . x ) A3: (dom f) /\ Y c= (dom f) /\ X by A2, XBOOLE_1:26; assume x in Y /\ (dom (f | Y)) ; ::_thesis: a >= (f | Y) . x 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 a >= (f | Y) . x by A4, FUNCT_1:47; ::_thesis: verum end; hence (f | Y) | Y is bounded_above by RFUNCT_1:70; ::_thesis: verum end; theorem :: INTEGRA2:6 for X, Y being non empty set for f being 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 ; ::_thesis: for f being PartFunc of X,REAL st f | X is bounded_below & Y c= X holds (f | Y) | Y is bounded_below let f be PartFunc of X,REAL; ::_thesis: ( f | X is bounded_below & Y c= X implies (f | Y) | Y is bounded_below ) assume f | X is bounded_below ; ::_thesis: ( not Y c= X or (f | Y) | Y is bounded_below ) then consider a being real number such that A1: for x being set st x in X /\ (dom f) holds f . x >= a by RFUNCT_1:71; assume A2: Y c= X ; ::_thesis: (f | Y) | Y is bounded_below for x being set st x in Y /\ (dom (f | Y)) holds (f | Y) . x >= a proof let x be set ; ::_thesis: ( x in Y /\ (dom (f | Y)) implies (f | Y) . x >= a ) A3: (dom f) /\ Y c= (dom f) /\ X by A2, XBOOLE_1:26; assume x in Y /\ (dom (f | Y)) ; ::_thesis: (f | Y) . x >= a 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 (f | Y) . x >= a by A4, FUNCT_1:47; ::_thesis: verum end; hence (f | Y) | Y is bounded_below by RFUNCT_1:71; ::_thesis: verum end; theorem :: INTEGRA2:7 for X being real-membered set for a being real number holds ( X is empty iff a ** X is empty ) ; theorem Th8: :: INTEGRA2:8 for r being Real for X being Subset of REAL holds r ** X = { (r * x) where x is Real : x in X } proof let r be Real; ::_thesis: for X being Subset of REAL holds r ** X = { (r * x) where x is Real : x in X } let X be Subset of REAL; ::_thesis: r ** X = { (r * x) where x is Real : x in X } thus r ** X c= { (r * x) where x is Real : x in X } :: according to XBOOLE_0:def_10 ::_thesis: { (r * x) where x is Real : x in X } c= r ** X proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in r ** X or y in { (r * x) where x is Real : x in X } ) assume y in r ** X ; ::_thesis: y in { (r * x) where x is Real : x in 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 y in { (r * x) where x is Real : x in X } by A1; ::_thesis: verum end; let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (r * x) where x is Real : x in X } or y in r ** X ) assume y in { (r * x) where x is Real : x in X } ; ::_thesis: y in r ** X then consider z being Real such that A2: ( y = r * z & z in X ) ; thus y in r ** X by A2, MEMBER_1:193; ::_thesis: verum end; theorem :: INTEGRA2:9 for r being Real for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds r ** X is bounded_above proof let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds r ** X is bounded_above let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above & 0 <= r implies r ** X is bounded_above ) assume that A1: X is bounded_above and A2: 0 <= r ; ::_thesis: r ** X is bounded_above consider b being real number such that A3: b is UpperBound of X by A1, XXREAL_2:def_10; A4: for x being real number st x in X holds x <= b by A3, XXREAL_2:def_1; r * b is UpperBound of r ** X proof let y be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not y in r ** X or y <= r * b ) assume y in r ** X ; ::_thesis: y <= r * b then y in { (r * x) where x is Real : x in X } by Th8; then consider x being Real such that A5: y = r * x and A6: x in X ; x <= b by A4, A6; hence y <= r * b by A2, A5, XREAL_1:64; ::_thesis: verum end; hence r ** X is bounded_above by XXREAL_2:def_10; ::_thesis: verum end; theorem :: INTEGRA2:10 for r being Real for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds r ** X is bounded_below proof let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds r ** X is bounded_below let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above & r <= 0 implies r ** X is bounded_below ) assume that A1: X is bounded_above and A2: r <= 0 ; ::_thesis: r ** X is bounded_below consider b being real number such that A3: b is UpperBound of X by A1, XXREAL_2:def_10; A4: for x being real number st x in X holds x <= b by A3, XXREAL_2:def_1; r * b is LowerBound of r ** X proof let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not y in r ** X or r * b <= y ) assume y in r ** X ; ::_thesis: r * b <= y then y in { (r * x) where x is Real : x in X } by Th8; then ex x being Real st ( y = r * x & x in X ) ; hence r * b <= y by A2, A4, XREAL_1:65; ::_thesis: verum end; hence r ** X is bounded_below by XXREAL_2:def_9; ::_thesis: verum end; theorem :: INTEGRA2:11 for r being Real for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds r ** X is bounded_below proof let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds r ** X is bounded_below let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below & 0 <= r implies r ** X is bounded_below ) assume that A1: X is bounded_below and A2: 0 <= r ; ::_thesis: r ** X is bounded_below consider b being real number such that A3: b is LowerBound of X by A1, XXREAL_2:def_9; A4: for x being real number st x in X holds b <= x by A3, XXREAL_2:def_2; r * b is LowerBound of r ** X proof let y be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not y in r ** X or r * b <= y ) assume y in r ** X ; ::_thesis: r * b <= y then y in { (r * x) where x is Real : x in X } by Th8; then ex x being Real st ( y = r * x & x in X ) ; hence r * b <= y by A2, A4, XREAL_1:64; ::_thesis: verum end; hence r ** X is bounded_below by XXREAL_2:def_9; ::_thesis: verum end; theorem :: INTEGRA2:12 for r being Real for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds r ** X is bounded_above proof let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds r ** X is bounded_above let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below & r <= 0 implies r ** X is bounded_above ) assume that A1: X is bounded_below and A2: r <= 0 ; ::_thesis: r ** X is bounded_above consider b being real number such that A3: b is LowerBound of X by A1, XXREAL_2:def_9; A4: for x being real number st x in X holds b <= x by A3, XXREAL_2:def_2; r * b is UpperBound of r ** X proof let y be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not y in r ** X or y <= r * b ) assume y in r ** X ; ::_thesis: y <= r * b then y in { (r * x) where x is Real : x in X } by Th8; then consider x being Real such that A5: y = r * x and A6: x in X ; b <= x by A4, A6; hence y <= r * b by A2, A5, XREAL_1:65; ::_thesis: verum end; hence r ** X is bounded_above by XXREAL_2:def_10; ::_thesis: verum end; theorem Th13: :: INTEGRA2:13 for r being Real for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds upper_bound (r ** X) = r * (upper_bound X) proof let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above & 0 <= r holds upper_bound (r ** X) = r * (upper_bound X) let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above & 0 <= r implies upper_bound (r ** X) = r * (upper_bound X) ) assume that A1: X is bounded_above and A2: 0 <= r ; ::_thesis: upper_bound (r ** X) = r * (upper_bound X) A3: for a being real number st a in r ** X holds a <= r * (upper_bound X) proof let a be real number ; ::_thesis: ( a in r ** X implies a <= r * (upper_bound X) ) assume a in r ** X ; ::_thesis: a <= r * (upper_bound X) then a in { (r * x) where x is Real : x in X } by Th8; then consider x being Real such that A4: a = r * x and A5: x in X ; x <= upper_bound X by A1, A5, SEQ_4:def_1; hence a <= r * (upper_bound X) by A2, A4, XREAL_1:64; ::_thesis: verum end; for b being real number st ( for a being real number st a in r ** X holds a <= b ) holds r * (upper_bound X) <= b proof consider x being Real such that A6: x in X by SUBSET_1:4; let b be real number ; ::_thesis: ( ( for a being real number st a in r ** X holds a <= b ) implies r * (upper_bound X) <= b ) assume A7: for a being real number st a in r ** X holds a <= b ; ::_thesis: r * (upper_bound X) <= b r * x in { (r * y) where y is Real : y in X } by A6; then A8: r * x in r ** X by Th8; now__::_thesis:_r_*_(upper_bound_X)_<=_b percases ( r = 0 or r > 0 ) by A2; suppose r = 0 ; ::_thesis: r * (upper_bound X) <= b hence r * (upper_bound X) <= b by A7, A8; ::_thesis: verum end; supposeA9: r > 0 ; ::_thesis: r * (upper_bound X) <= b for z being real number st z in X holds z <= b / r proof let z be real number ; ::_thesis: ( z in X implies z <= b / r ) assume z in X ; ::_thesis: z <= b / r then r * z in { (r * y) where y is Real : y in X } ; then r * z in r ** X by Th8; hence z <= b / r by A7, A9, XREAL_1:77; ::_thesis: verum 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 r * (upper_bound X) <= b by A9, XCMPLX_1:87; ::_thesis: verum end; end; end; hence r * (upper_bound X) <= b ; ::_thesis: verum end; hence upper_bound (r ** X) = r * (upper_bound X) by A3, SEQ_4:46; ::_thesis: verum end; theorem Th14: :: INTEGRA2:14 for r being Real for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds lower_bound (r ** X) = r * (upper_bound X) proof let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_above & r <= 0 holds lower_bound (r ** X) = r * (upper_bound X) let X be non empty Subset of REAL; ::_thesis: ( X is bounded_above & r <= 0 implies lower_bound (r ** X) = r * (upper_bound X) ) assume that A1: X is bounded_above and A2: r <= 0 ; ::_thesis: lower_bound (r ** X) = r * (upper_bound X) A3: for a being real number st a in r ** X holds r * (upper_bound X) <= a proof let a be real number ; ::_thesis: ( a in r ** X implies r * (upper_bound X) <= a ) assume a in r ** X ; ::_thesis: r * (upper_bound X) <= a then a in { (r * x) where x is Real : x in X } by Th8; then consider x being Real such that A4: a = r * x and A5: x in X ; x <= upper_bound X by A1, A5, SEQ_4:def_1; hence r * (upper_bound X) <= a by A2, A4, XREAL_1:65; ::_thesis: verum end; for b being real number st ( for a being real number st a in r ** X holds a >= b ) holds r * (upper_bound X) >= b proof consider x being Real such that A6: x in X by SUBSET_1:4; let b be real number ; ::_thesis: ( ( for a being real number st a in r ** X holds a >= b ) implies r * (upper_bound X) >= b ) assume A7: for a being real number st a in r ** X holds a >= b ; ::_thesis: r * (upper_bound X) >= b r * x in { (r * y) where y is Real : y in X } by A6; then A8: r * x in r ** X by Th8; now__::_thesis:_r_*_(upper_bound_X)_>=_b percases ( r = 0 or r < 0 ) by A2; suppose r = 0 ; ::_thesis: r * (upper_bound X) >= b hence r * (upper_bound X) >= b by A7, A8; ::_thesis: verum end; supposeA9: r < 0 ; ::_thesis: r * (upper_bound X) >= b for z being real number st z in X holds z <= b / r proof let z be real number ; ::_thesis: ( z in X implies z <= b / r ) assume z in X ; ::_thesis: z <= b / r then r * z in { (r * y) where y is Real : y in X } ; then r * z in r ** X by Th8; hence z <= b / r by A7, A9, XREAL_1:80; ::_thesis: verum 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 r * (upper_bound X) >= b by A9, XCMPLX_1:87; ::_thesis: verum end; end; end; hence r * (upper_bound X) >= b ; ::_thesis: verum end; hence lower_bound (r ** X) = r * (upper_bound X) by A3, SEQ_4:44; ::_thesis: verum end; theorem Th15: :: INTEGRA2:15 for r being Real for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds lower_bound (r ** X) = r * (lower_bound X) proof let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below & 0 <= r holds lower_bound (r ** X) = r * (lower_bound X) let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below & 0 <= r implies lower_bound (r ** X) = r * (lower_bound X) ) assume that A1: X is bounded_below and A2: 0 <= r ; ::_thesis: lower_bound (r ** X) = r * (lower_bound X) A3: for a being real number st a in r ** X holds r * (lower_bound X) <= a proof let a be real number ; ::_thesis: ( a in r ** X implies r * (lower_bound X) <= a ) assume a in r ** X ; ::_thesis: r * (lower_bound X) <= a then a in { (r * x) where x is Real : x in X } by Th8; then consider x being Real such that A4: a = r * x and A5: x in X ; lower_bound X <= x by A1, A5, SEQ_4:def_2; hence r * (lower_bound X) <= a by A2, A4, XREAL_1:64; ::_thesis: verum end; for b being real number st ( for a being real number st a in r ** X holds a >= b ) holds r * (lower_bound X) >= b proof consider x being Real such that A6: x in X by SUBSET_1:4; let b be real number ; ::_thesis: ( ( for a being real number st a in r ** X holds a >= b ) implies r * (lower_bound X) >= b ) assume A7: for a being real number st a in r ** X holds a >= b ; ::_thesis: r * (lower_bound X) >= b r * x in { (r * y) where y is Real : y in X } by A6; then A8: r * x in r ** X by Th8; now__::_thesis:_r_*_(lower_bound_X)_>=_b percases ( r = 0 or r > 0 ) by A2; suppose r = 0 ; ::_thesis: r * (lower_bound X) >= b hence r * (lower_bound X) >= b by A7, A8; ::_thesis: verum end; supposeA9: r > 0 ; ::_thesis: r * (lower_bound X) >= b for z being real number st z in X holds z >= b / r proof let z be real number ; ::_thesis: ( z in X implies z >= b / r ) assume z in X ; ::_thesis: z >= b / r then r * z in { (r * y) where y is Real : y in X } ; then r * z in r ** X by Th8; hence z >= b / r by A7, A9, XREAL_1:79; ::_thesis: verum 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 r * (lower_bound X) >= b by A9, XCMPLX_1:87; ::_thesis: verum end; end; end; hence r * (lower_bound X) >= b ; ::_thesis: verum end; hence lower_bound (r ** X) = r * (lower_bound X) by A3, SEQ_4:44; ::_thesis: verum end; theorem Th16: :: INTEGRA2:16 for r being Real for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds upper_bound (r ** X) = r * (lower_bound X) proof let r be Real; ::_thesis: for X being non empty Subset of REAL st X is bounded_below & r <= 0 holds upper_bound (r ** X) = r * (lower_bound X) let X be non empty Subset of REAL; ::_thesis: ( X is bounded_below & r <= 0 implies upper_bound (r ** X) = r * (lower_bound X) ) assume that A1: X is bounded_below and A2: r <= 0 ; ::_thesis: upper_bound (r ** X) = r * (lower_bound X) A3: for a being real number st a in r ** X holds r * (lower_bound X) >= a proof let a be real number ; ::_thesis: ( a in r ** X implies r * (lower_bound X) >= a ) assume a in r ** X ; ::_thesis: r * (lower_bound X) >= a then a in { (r * x) where x is Real : x in X } by Th8; then consider x being Real such that A4: a = r * x and A5: x in X ; lower_bound X <= x by A1, A5, SEQ_4:def_2; hence r * (lower_bound X) >= a by A2, A4, XREAL_1:65; ::_thesis: verum end; for b being real number st ( for a being real number st a in r ** X holds a <= b ) holds r * (lower_bound X) <= b proof consider x being Real such that A6: x in X by SUBSET_1:4; let b be real number ; ::_thesis: ( ( for a being real number st a in r ** X holds a <= b ) implies r * (lower_bound X) <= b ) assume A7: for a being real number st a in r ** X holds a <= b ; ::_thesis: r * (lower_bound X) <= b r * x in { (r * y) where y is Real : y in X } by A6; then A8: r * x in r ** X by Th8; now__::_thesis:_r_*_(lower_bound_X)_<=_b percases ( r = 0 or r < 0 ) by A2; suppose r = 0 ; ::_thesis: r * (lower_bound X) <= b hence r * (lower_bound X) <= b by A7, A8; ::_thesis: verum end; supposeA9: r < 0 ; ::_thesis: r * (lower_bound X) <= b for z being real number st z in X holds z >= b / r proof let z be real number ; ::_thesis: ( z in X implies z >= b / r ) assume z in X ; ::_thesis: z >= b / r then r * z in { (r * y) where y is Real : y in X } ; then r * z in r ** X by Th8; hence z >= b / r by A7, A9, XREAL_1:78; ::_thesis: verum 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 r * (lower_bound X) <= b by A9, XCMPLX_1:87; ::_thesis: verum end; end; end; hence r * (lower_bound X) <= b ; ::_thesis: verum end; hence upper_bound (r ** X) = r * (lower_bound X) by A3, SEQ_4:46; ::_thesis: verum end; begin theorem Th17: :: INTEGRA2:17 for r being Real for X being non empty set for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f) proof let r be Real; ::_thesis: for X being non empty set for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f) let X be non empty set ; ::_thesis: for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f) let f be Function of X,REAL; ::_thesis: rng (r (#) f) = r ** (rng f) for y being Real st y in r ** (rng f) holds y in rng (r (#) f) proof let y be Real; ::_thesis: ( y in r ** (rng f) implies y in rng (r (#) f) ) assume y in r ** (rng f) ; ::_thesis: y in rng (r (#) f) then y in { (r * b) where b is Real : b in rng f } by Th8; then consider b being Real 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 y in rng (r (#) f) by A1, A4, RFUNCT_1:57; ::_thesis: verum end; then A5: r ** (rng f) c= rng (r (#) f) by SUBSET_1:2; for y being Real st y in rng (r (#) f) holds y in r ** (rng f) proof let y be Real; ::_thesis: ( y in rng (r (#) f) implies y in r ** (rng f) ) assume y in rng (r (#) f) ; ::_thesis: y in r ** (rng 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; y = r * (f . x) by A7, RFUNCT_1:57; then y in { (r * b) where b is Real : b in rng f } by A8; hence y in r ** (rng f) by Th8; ::_thesis: verum end; then rng (r (#) f) c= r ** (rng f) by SUBSET_1:2; hence rng (r (#) f) = r ** (rng f) by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th18: :: INTEGRA2:18 for r being Real for X, Z being non empty set for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z)) proof let r be Real; ::_thesis: for X, Z being non empty set for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z)) let X, Z be non empty set ; ::_thesis: for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z)) let f be PartFunc of X,REAL; ::_thesis: rng (r (#) (f | Z)) = r ** (rng (f | Z)) for y being Real st y in r ** (rng (f | Z)) holds y in rng (r (#) (f | Z)) proof let y be Real; ::_thesis: ( y in r ** (rng (f | Z)) implies y in rng (r (#) (f | Z)) ) assume y in r ** (rng (f | Z)) ; ::_thesis: y in rng (r (#) (f | Z)) then y in { (r * b) where b is Real : b in rng (f | Z) } by Th8; then consider b being Real 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 y in rng (r (#) (f | Z)) by A5, FUNCT_1:def_3; ::_thesis: verum end; then A6: r ** (rng (f | Z)) c= rng (r (#) (f | Z)) by SUBSET_1:2; for y being Real st y in rng (r (#) (f | Z)) holds y in r ** (rng (f | Z)) proof let y be Real; ::_thesis: ( y in rng (r (#) (f | Z)) implies y in r ** (rng (f | Z)) ) assume y in rng (r (#) (f | Z)) ; ::_thesis: y in r ** (rng (f | Z)) then consider x being 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; y = r * ((f | Z) . x) by A7, A8, VALUED_1:def_5; then y in { (r * b) where b is Real : b in rng (f | Z) } by A9; hence y in r ** (rng (f | Z)) by Th8; ::_thesis: verum end; then rng (r (#) (f | Z)) c= r ** (rng (f | Z)) by SUBSET_1:2; hence rng (r (#) (f | Z)) = r ** (rng (f | Z)) by A6, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th19: :: INTEGRA2:19 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded & r >= 0 holds (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded & r >= 0 holds (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st f | A is bounded & r >= 0 holds (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded & r >= 0 holds (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) let D be Division of A; ::_thesis: ( f | A is bounded & r >= 0 implies (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) ) assume that A1: f | A is bounded and A2: r >= 0 ; ::_thesis: (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) 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 (upper_sum_set (r (#) f)) . D >= (r * (lower_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; ::_thesis: verum end; theorem Th20: :: INTEGRA2:20 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded & r <= 0 holds (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded & r <= 0 holds (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st f | A is bounded & r <= 0 holds (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded & r <= 0 holds (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) let D be Division of A; ::_thesis: ( f | A is bounded & r <= 0 implies (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) ) assume that A1: f | A is bounded and A2: r <= 0 ; ::_thesis: (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) 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 (upper_sum_set (r (#) f)) . D >= (r * (upper_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; ::_thesis: verum end; theorem Th21: :: INTEGRA2:21 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded & r >= 0 holds (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded & r >= 0 holds (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st f | A is bounded & r >= 0 holds (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded & r >= 0 holds (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) let D be Division of A; ::_thesis: ( f | A is bounded & r >= 0 implies (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) ) assume that A1: f | A is bounded and A2: r >= 0 ; ::_thesis: (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) 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 (lower_sum_set (r (#) f)) . D <= (r * (upper_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; ::_thesis: verum end; theorem Th22: :: INTEGRA2:22 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded & r <= 0 holds (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded & r <= 0 holds (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st f | A is bounded & r <= 0 holds (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded & r <= 0 holds (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) let D be Division of A; ::_thesis: ( f | A is bounded & r <= 0 implies (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) ) assume that A1: f | A is bounded and A2: r <= 0 ; ::_thesis: (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) 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 (lower_sum_set (r (#) f)) . D <= (r * (lower_bound (rng f))) * (vol A) by A6, A5, XXREAL_0:2; ::_thesis: verum end; theorem Th23: :: INTEGRA2:23 for r being Real for i being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) proof let r be Real; ::_thesis: for i being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) let i be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) let f be Function of A,REAL; ::_thesis: for D being Division of A st i in dom D & f | A is bounded_above & r >= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) let D be Division of A; ::_thesis: ( i in dom D & f | A is bounded_above & r >= 0 implies (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) ) assume that A1: i in dom D and A2: f | A is bounded_above and A3: r >= 0 ; ::_thesis: (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) 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: not rng (f | (divset (D,i))) is 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 (upper_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) ; ::_thesis: verum end; theorem Th24: :: INTEGRA2:24 for r being Real for i being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) proof let r be Real; ::_thesis: for i being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) let i be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) let f be Function of A,REAL; ::_thesis: for D being Division of A st i in dom D & f | A is bounded_above & r <= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) let D be Division of A; ::_thesis: ( i in dom D & f | A is bounded_above & r <= 0 implies (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) ) assume that A1: i in dom D and A2: f | A is bounded_above and A3: r <= 0 ; ::_thesis: (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) 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: not rng (f | (divset (D,i))) is 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 (lower_volume ((r (#) f),D)) . i = r * ((upper_volume (f,D)) . i) ; ::_thesis: verum end; theorem Th25: :: INTEGRA2:25 for r being Real for i being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) proof let r be Real; ::_thesis: for i being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) let i be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) let f be Function of A,REAL; ::_thesis: for D being Division of A st i in dom D & f | A is bounded_below & r >= 0 holds (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) let D be Division of A; ::_thesis: ( i in dom D & f | A is bounded_below & r >= 0 implies (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) ) assume that A1: i in dom D and A2: f | A is bounded_below and A3: r >= 0 ; ::_thesis: (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) 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: not rng (f | (divset (D,i))) is 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 (lower_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) ; ::_thesis: verum end; theorem Th26: :: INTEGRA2:26 for r being Real for i being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) proof let r be Real; ::_thesis: for i being Element of NAT for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) let i be Element of NAT ; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) let f be Function of A,REAL; ::_thesis: for D being Division of A st i in dom D & f | A is bounded_below & r <= 0 holds (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) let D be Division of A; ::_thesis: ( i in dom D & f | A is bounded_below & r <= 0 implies (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) ) assume that A1: i in dom D and A2: f | A is bounded_below and A3: r <= 0 ; ::_thesis: (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) 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: not rng (f | (divset (D,i))) is 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 (upper_volume ((r (#) f),D)) . i = r * ((lower_volume (f,D)) . i) ; ::_thesis: verum end; theorem Th27: :: INTEGRA2:27 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded_above & r >= 0 holds upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded_above & r >= 0 holds upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st f | A is bounded_above & r >= 0 holds upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded_above & r >= 0 holds upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) let D be Division of A; ::_thesis: ( f | A is bounded_above & r >= 0 implies upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) ) assume A1: ( f | A is bounded_above & r >= 0 ) ; ::_thesis: upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) A2: for i being 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; ::_thesis: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) implies (upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i ) assume A3: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) ) ; ::_thesis: (upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i 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 (upper_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i ; ::_thesis: verum 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 upper_sum ((r (#) f),D) = r * (upper_sum (f,D)) ; ::_thesis: verum end; theorem Th28: :: INTEGRA2:28 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded_above & r <= 0 holds lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded_above & r <= 0 holds lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st f | A is bounded_above & r <= 0 holds lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded_above & r <= 0 holds lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) let D be Division of A; ::_thesis: ( f | A is bounded_above & r <= 0 implies lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) ) assume A1: ( f | A is bounded_above & r <= 0 ) ; ::_thesis: lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) A2: for i being 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; ::_thesis: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) implies (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i ) assume A3: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) ) ; ::_thesis: (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i 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 (lower_volume ((r (#) f),D)) . i = (r * (upper_volume (f,D))) . i ; ::_thesis: verum 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 lower_sum ((r (#) f),D) = r * (upper_sum (f,D)) ; ::_thesis: verum end; theorem Th29: :: INTEGRA2:29 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded_below & r >= 0 holds lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded_below & r >= 0 holds lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st f | A is bounded_below & r >= 0 holds lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded_below & r >= 0 holds lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) let D be Division of A; ::_thesis: ( f | A is bounded_below & r >= 0 implies lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) ) assume A1: ( f | A is bounded_below & r >= 0 ) ; ::_thesis: lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) A2: for i being 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; ::_thesis: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) implies (lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ) assume A3: ( 1 <= i & i <= len (lower_volume ((r (#) f),D)) ) ; ::_thesis: (lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i 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 (lower_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ; ::_thesis: verum 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 lower_sum ((r (#) f),D) = r * (lower_sum (f,D)) ; ::_thesis: verum end; theorem Th30: :: INTEGRA2:30 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded_below & r <= 0 holds upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL for D being Division of A st f | A is bounded_below & r <= 0 holds upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL for D being Division of A st f | A is bounded_below & r <= 0 holds upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) let f be Function of A,REAL; ::_thesis: for D being Division of A st f | A is bounded_below & r <= 0 holds upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) let D be Division of A; ::_thesis: ( f | A is bounded_below & r <= 0 implies upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) ) assume A1: ( f | A is bounded_below & r <= 0 ) ; ::_thesis: upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) A2: for i being 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; ::_thesis: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) implies (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ) assume A3: ( 1 <= i & i <= len (upper_volume ((r (#) f),D)) ) ; ::_thesis: (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i 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 (upper_volume ((r (#) f),D)) . i = (r * (lower_volume (f,D))) . i ; ::_thesis: verum 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 upper_sum ((r (#) f),D) = r * (lower_sum (f,D)) ; ::_thesis: verum end; theorem Th31: :: INTEGRA2:31 for r being Real for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded & f is integrable holds ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) proof let r be Real; ::_thesis: for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded & f is integrable holds ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) let f be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable implies ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) ) assume that A1: f | A is bounded and A2: f is integrable ; ::_thesis: ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) 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__::_thesis:_(_upper_integral_(r_(#)_f)_=_lower_integral_(r_(#)_f)_&_upper_integral_(r_(#)_f)_=_r_*_(integral_f)_) percases ( r >= 0 or r < 0 ) ; supposeA6: r >= 0 ; ::_thesis: ( upper_integral (r (#) f) = lower_integral (r (#) f) & upper_integral (r (#) f) = r * (integral f) ) A7: for D being set st D in divs A holds (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D proof let D be set ; ::_thesis: ( D in divs A implies (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ) assume A8: D in divs A ; ::_thesis: (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D then reconsider D = 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 (upper_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; ::_thesis: verum 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 being set st D in divs A holds (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D proof let D be set ; ::_thesis: ( D in divs A implies (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ) assume A12: D in divs A ; ::_thesis: (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D then reconsider D = 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 (lower_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; ::_thesis: verum 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; ::_thesis: upper_integral (r (#) f) = r * (integral f) thus upper_integral (r (#) f) = r * (integral f) by A10, INTEGRA1:def_17; ::_thesis: verum end; supposeA14: r < 0 ; ::_thesis: ( upper_integral (r (#) f) = lower_integral (r (#) f) & upper_integral (r (#) f) = r * (integral f) ) A15: for D being set st D in divs A holds (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D proof let D be set ; ::_thesis: ( D in divs A implies (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ) assume A16: D in divs A ; ::_thesis: (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D then reconsider D = 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 (upper_sum_set (r (#) f)) . D = (r (#) (lower_sum_set f)) . D ; ::_thesis: verum 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 being set st D in divs A holds (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D proof let D be set ; ::_thesis: ( D in divs A implies (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ) assume A20: D in divs A ; ::_thesis: (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D then reconsider D = 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 (lower_sum_set (r (#) f)) . D = (r (#) (upper_sum_set f)) . D ; ::_thesis: verum 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; ::_thesis: upper_integral (r (#) f) = r * (integral f) 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) ; ::_thesis: verum end; end; end; ex a being Real st for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds a >= (lower_sum_set (r (#) f)) . D proof now__::_thesis:_ex_a_being_Real_st_ for_D_being_set_st_D_in_(divs_A)_/\_(dom_(lower_sum_set_(r_(#)_f)))_holds_ a_>=_(lower_sum_set_(r_(#)_f))_._D percases ( r >= 0 or r < 0 ) ; supposeA22: r >= 0 ; ::_thesis: ex a being Real st for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds a >= (lower_sum_set (r (#) f)) . D for D being set 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 set ; ::_thesis: ( D in (divs A) /\ (dom (lower_sum_set (r (#) f))) implies (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D ) assume D in (divs A) /\ (dom (lower_sum_set (r (#) f))) ; ::_thesis: (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D then D is Division of A by INTEGRA1:def_3; hence (r * (upper_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D by A1, A22, Th21; ::_thesis: verum end; hence ex a being Real st for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds a >= (lower_sum_set (r (#) f)) . D ; ::_thesis: verum end; supposeA23: r < 0 ; ::_thesis: ex a being Real st for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds a >= (lower_sum_set (r (#) f)) . D for D being set 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 set ; ::_thesis: ( D in (divs A) /\ (dom (lower_sum_set (r (#) f))) implies (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D ) assume D in (divs A) /\ (dom (lower_sum_set (r (#) f))) ; ::_thesis: (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D then D is Division of A by INTEGRA1:def_3; hence (r * (lower_bound (rng f))) * (vol A) >= (lower_sum_set (r (#) f)) . D by A1, A23, Th22; ::_thesis: verum end; hence ex a being Real st for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds a >= (lower_sum_set (r (#) f)) . D ; ::_thesis: verum end; end; end; hence ex a being Real st for D being set st D in (divs A) /\ (dom (lower_sum_set (r (#) f))) holds a >= (lower_sum_set (r (#) f)) . D ; ::_thesis: verum 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 being Real st for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds a <= (upper_sum_set (r (#) f)) . D proof now__::_thesis:_ex_a_being_Real_st_ for_D_being_set_st_D_in_(divs_A)_/\_(dom_(upper_sum_set_(r_(#)_f)))_holds_ a_<=_(upper_sum_set_(r_(#)_f))_._D percases ( r >= 0 or r < 0 ) ; supposeA25: r >= 0 ; ::_thesis: ex a being Real st for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds a <= (upper_sum_set (r (#) f)) . D for D being set 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 set ; ::_thesis: ( D in (divs A) /\ (dom (upper_sum_set (r (#) f))) implies (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D ) assume D in (divs A) /\ (dom (upper_sum_set (r (#) f))) ; ::_thesis: (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D then D is Division of A by INTEGRA1:def_3; hence (r * (lower_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D by A1, A25, Th19; ::_thesis: verum end; hence ex a being Real st for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds a <= (upper_sum_set (r (#) f)) . D ; ::_thesis: verum end; supposeA26: r < 0 ; ::_thesis: ex a being Real st for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds a <= (upper_sum_set (r (#) f)) . D for D being set 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 set ; ::_thesis: ( D in (divs A) /\ (dom (upper_sum_set (r (#) f))) implies (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D ) assume D in (divs A) /\ (dom (upper_sum_set (r (#) f))) ; ::_thesis: (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D then D is Division of A by INTEGRA1:def_3; hence (r * (upper_bound (rng f))) * (vol A) <= (upper_sum_set (r (#) f)) . D by A1, A26, Th20; ::_thesis: verum end; hence ex a being Real st for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds a <= (upper_sum_set (r (#) f)) . D ; ::_thesis: verum end; end; end; hence ex a being Real st for D being set st D in (divs A) /\ (dom (upper_sum_set (r (#) f))) holds a <= (upper_sum_set (r (#) f)) . D ; ::_thesis: verum 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 ( r (#) f is integrable & integral (r (#) f) = r * (integral f) ) by A24, A5, INTEGRA1:def_16, INTEGRA1:def_17; ::_thesis: verum end; begin theorem Th32: :: INTEGRA2:32 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded & ( for x being Real st x in A holds f . x >= 0 ) holds integral f >= 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded & ( for x being Real st x in A holds f . x >= 0 ) holds integral f >= 0 let f be Function of A,REAL; ::_thesis: ( f | A is bounded & ( for x being Real st x in A holds f . x >= 0 ) implies integral f >= 0 ) assume that A1: f | A is bounded and A2: for x being Real st x in A holds f . x >= 0 ; ::_thesis: integral f >= 0 A3: for a being real number st a in rng (upper_sum_set f) holds a >= 0 proof let a be real number ; ::_thesis: ( a in rng (upper_sum_set f) implies a >= 0 ) assume a in rng (upper_sum_set f) ; ::_thesis: a >= 0 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 = D as Division of A by INTEGRA1:def_3; A5: for i being Nat st i in dom (upper_volume (f,D)) holds 0 <= (upper_volume (f,D)) . i proof let i be Nat; ::_thesis: ( i in dom (upper_volume (f,D)) implies 0 <= (upper_volume (f,D)) . i ) set r = (upper_volume (f,D)) . i; assume A6: i in dom (upper_volume (f,D)) ; ::_thesis: 0 <= (upper_volume (f,D)) . i 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 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 upper_bound (rng (f | (divset (D,i)))) >= 0 by A9, A11, SEQ_4:def_1; ::_thesis: verum end; A12: vol (divset (D,i)) >= 0 by INTEGRA1:9; (upper_volume (f,D)) . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) by A7, INTEGRA1:def_6; hence 0 <= (upper_volume (f,D)) . i by A12, A8; ::_thesis: verum end; a = upper_sum (f,D) by A4, INTEGRA1:def_10 .= Sum (upper_volume (f,D)) by INTEGRA1:def_8 ; hence a >= 0 by A5, RVSUM_1:84; ::_thesis: verum end; ( upper_integral f = lower_bound (rng (upper_sum_set f)) & not rng (upper_sum_set f) is empty ) by INTEGRA1:def_14; then upper_integral f >= 0 by A3, SEQ_4:43; hence integral f >= 0 by INTEGRA1:def_17; ::_thesis: verum end; theorem Th33: :: INTEGRA2:33 for A being non empty closed_interval Subset of REAL for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds ( f - g is integrable & integral (f - g) = (integral f) - (integral g) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable holds ( f - g is integrable & integral (f - g) = (integral f) - (integral g) ) let f, g be Function of A,REAL; ::_thesis: ( 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) ) ) assume that A1: ( f | A is bounded & f is integrable ) and A2: g | A is bounded and A3: g is integrable ; ::_thesis: ( f - g is integrable & integral (f - g) = (integral f) - (integral g) ) - g = (- 1) (#) g ; then 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; ::_thesis: integral (f - g) = (integral f) - (integral g) integral (- g) = (- 1) * (integral g) by A2, A3, Th31; then integral (f - g) = (integral f) + (- (integral g)) by A1, A5, A4, INTEGRA1:57; hence integral (f - g) = (integral f) - (integral g) ; ::_thesis: verum end; theorem :: INTEGRA2:34 for A being non empty closed_interval Subset of REAL for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds f . x >= g . x ) holds integral f >= integral g proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f, g being Function of A,REAL st f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds f . x >= g . x ) holds integral f >= integral g let f, g be Function of A,REAL; ::_thesis: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable & ( for x being Real st x in A holds f . x >= g . x ) implies integral f >= integral g ) assume that A1: ( f | A is bounded & f is integrable & g | A is bounded & g is integrable ) and A2: for x being Real st x in A holds f . x >= g . x ; ::_thesis: integral f >= integral g A3: dom (f - g) = A by FUNCT_2:def_1; A4: for x being Real st x in A holds (f - g) . x >= 0 proof let x be Real; ::_thesis: ( x in A implies (f - g) . x >= 0 ) assume A5: x in A ; ::_thesis: (f - g) . x >= 0 then (f - g) . x = (f . x) - (g . x) by A3, VALUED_1:13; hence (f - g) . x >= 0 by A2, A5, XREAL_1:48; ::_thesis: verum end; ( integral (f - g) = (integral f) - (integral g) & (f - g) | (A /\ A) is bounded ) by A1, Th33, RFUNCT_1:84; hence integral f >= integral g by A4, Th32, XREAL_1:49; ::_thesis: verum end; begin theorem :: INTEGRA2:35 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded holds rng (upper_sum_set f) is bounded_below proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded holds rng (upper_sum_set f) is bounded_below let f be Function of A,REAL; ::_thesis: ( f | A is bounded implies rng (upper_sum_set f) is bounded_below ) set D1 = the Division of A; assume A1: f | A is bounded ; ::_thesis: rng (upper_sum_set f) is bounded_below take lower_sum (f, the Division of A) ; :: according to XXREAL_2:def_9 ::_thesis: lower_sum (f, the Division of A) is LowerBound of rng (upper_sum_set f) let a be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not a in rng (upper_sum_set f) or lower_sum (f, the Division of A) <= a ) assume a in rng (upper_sum_set f) ; ::_thesis: lower_sum (f, the Division of A) <= a then consider D being 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 = D as Division of A by INTEGRA1:def_3; a = upper_sum (f,D) by A2, INTEGRA1:def_10; hence lower_sum (f, the Division of A) <= a by A1, INTEGRA1:48; ::_thesis: verum end; theorem :: INTEGRA2:36 for A being non empty closed_interval Subset of REAL for f being Function of A,REAL st f | A is bounded holds rng (lower_sum_set f) is bounded_above proof let A be non empty closed_interval Subset of REAL; ::_thesis: for f being Function of A,REAL st f | A is bounded holds rng (lower_sum_set f) is bounded_above let f be Function of A,REAL; ::_thesis: ( f | A is bounded implies rng (lower_sum_set f) is bounded_above ) set D1 = the Division of A; assume A1: f | A is bounded ; ::_thesis: rng (lower_sum_set f) is bounded_above take upper_sum (f, the Division of A) ; :: according to XXREAL_2:def_10 ::_thesis: upper_sum (f, the Division of A) is UpperBound of rng (lower_sum_set f) let a be ext-real number ; :: according to XXREAL_2:def_1 ::_thesis: ( not a in rng (lower_sum_set f) or a <= upper_sum (f, the Division of A) ) assume a in rng (lower_sum_set f) ; ::_thesis: a <= upper_sum (f, the Division of A) then consider D being 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 = D as Division of A by INTEGRA1:def_3; a = lower_sum (f,D) by A2, INTEGRA1:def_11; hence a <= upper_sum (f, the Division of A) by A1, INTEGRA1:48; ::_thesis: verum end; definition let A be non empty closed_interval Subset of REAL; mode DivSequence of A is Function of NAT,(divs A); end; definition let A be non empty closed_interval Subset of REAL; let T be DivSequence of A; let i be Element of NAT ; :: original: . redefine funcT . i -> Division of A; coherence T . i is Division of A proof T . i is Element of divs A ; hence T . i is Division of A by INTEGRA1:def_3; ::_thesis: verum end; end; definition let A be non empty closed_interval Subset of REAL; let f be PartFunc of A,REAL; let T be DivSequence of A; func upper_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 2 for i being Element of NAT holds it . i = upper_sum (f,(T . i)); existence ex b1 being Real_Sequence st for i being Element of NAT holds b1 . i = upper_sum (f,(T . i)) proof deffunc H1( Element of NAT ) -> Element of REAL = upper_sum (f,(T . \$1)); thus ex IT being Real_Sequence st for i being Element of NAT holds IT . i = H1(i) from SEQ_1:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = upper_sum (f,(T . i)) ) & ( for i being Element of NAT holds b2 . i = upper_sum (f,(T . i)) ) holds b1 = b2 proof let F1, F2 be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds F1 . i = upper_sum (f,(T . i)) ) & ( for i being Element of NAT holds F2 . i = upper_sum (f,(T . i)) ) implies F1 = F2 ) assume that A1: for i being Element of NAT holds F1 . i = upper_sum (f,(T . i)) and A2: for i being Element of NAT holds F2 . i = upper_sum (f,(T . i)) ; ::_thesis: F1 = F2 for i being Element of NAT holds F1 . i = F2 . i proof let i be Element of NAT ; ::_thesis: F1 . i = F2 . i F1 . i = upper_sum (f,(T . i)) by A1 .= F2 . i by A2 ; hence F1 . i = F2 . i ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; func lower_sum (f,T) -> Real_Sequence means :: INTEGRA2:def 3 for i being Element of NAT holds it . i = lower_sum (f,(T . i)); existence ex b1 being Real_Sequence st for i being Element of NAT holds b1 . i = lower_sum (f,(T . i)) proof deffunc H1( Element of NAT ) -> Element of REAL = lower_sum (f,(T . \$1)); thus ex IT being Real_Sequence st for i being Element of NAT holds IT . i = H1(i) from SEQ_1:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being Real_Sequence st ( for i being Element of NAT holds b1 . i = lower_sum (f,(T . i)) ) & ( for i being Element of NAT holds b2 . i = lower_sum (f,(T . i)) ) holds b1 = b2 proof let F1, F2 be Real_Sequence; ::_thesis: ( ( for i being Element of NAT holds F1 . i = lower_sum (f,(T . i)) ) & ( for i being Element of NAT holds F2 . i = lower_sum (f,(T . i)) ) implies F1 = F2 ) assume that A3: for i being Element of NAT holds F1 . i = lower_sum (f,(T . i)) and A4: for i being Element of NAT holds F2 . i = lower_sum (f,(T . i)) ; ::_thesis: F1 = F2 for i being Element of NAT holds F1 . i = F2 . i proof let i be Element of NAT ; ::_thesis: F1 . i = F2 . i F1 . i = lower_sum (f,(T . i)) by A3 .= F2 . i by A4 ; hence F1 . i = F2 . i ; ::_thesis: verum end; hence F1 = F2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines upper_sum INTEGRA2:def_2_:_ for A being non empty closed_interval Subset of REAL for f being PartFunc of A,REAL for T being DivSequence of A for b4 being Real_Sequence holds ( b4 = upper_sum (f,T) iff for i being Element of NAT holds b4 . i = upper_sum (f,(T . i)) ); :: deftheorem defines lower_sum INTEGRA2:def_3_:_ for A being non empty closed_interval Subset of REAL for f being PartFunc of A,REAL for T being DivSequence of A for b4 being Real_Sequence holds ( b4 = lower_sum (f,T) iff for i being Element of NAT holds b4 . i = lower_sum (f,(T . i)) ); theorem :: INTEGRA2:37 for A being non empty closed_interval Subset of REAL for D1, D2 being Division of A st D1 <= D2 holds for j being Element of NAT st j in dom D2 holds ex i being Element of NAT st ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for D1, D2 being Division of A st D1 <= D2 holds for j being Element of NAT st j in dom D2 holds ex i being Element of NAT st ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) let D1, D2 be Division of A; ::_thesis: ( D1 <= D2 implies for j being Element of NAT st j in dom D2 holds ex i being Element of NAT st ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) ) assume A1: D1 <= D2 ; ::_thesis: for j being Element of NAT st j in dom D2 holds ex i being Element of NAT st ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) let j be Element of NAT ; ::_thesis: ( j in dom D2 implies ex i being Element of NAT st ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) ) defpred S1[ set ] means ( D2 . \$1 in rng D1 & D2 . \$1 >= D2 . j ); consider X being Subset of (dom D2) such that A2: for x1 being set holds ( x1 in X iff ( x1 in dom D2 & S1[x1] ) ) from SUBSET_1:sch_1(); reconsider X = X as Subset of NAT by XBOOLE_1:1; assume A3: j in dom D2 ; ::_thesis: ex i being Element of NAT st ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) ex n being Element of NAT st ( n in dom D2 & D2 . n in rng D1 & D2 . n >= D2 . j ) proof take len D2 ; ::_thesis: ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j ) 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 ( len D2 in dom D2 & D2 . (len D2) in rng D1 & D2 . (len D2) >= D2 . j ) by A3, A5, A6, A4, FUNCT_1:def_3, SEQ_4:137; ::_thesis: verum end; then reconsider X = 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 ; ::_thesis: ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) A11: D1 . i >= D2 . j by A2, A7, A10; divset (D2,j) c= divset (D1,i) proof now__::_thesis:_divset_(D2,j)_c=_divset_(D1,i) percases ( i = 1 or i <> 1 ) ; suppose i = 1 ; ::_thesis: divset (D2,j) c= divset (D1,i) 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__::_thesis:_divset_(D2,j)_c=_divset_(D1,i) percases ( j = 1 or j <> 1 ) ; supposeA13: j = 1 ; ::_thesis: divset (D2,j) c= divset (D1,i) ( 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 where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A14, RCOMP_1:def_1; then ex x being Real st ( x = D1 . i & lower_bound A <= x & x <= upper_bound A ) ; then lower_bound A in { r where r is Real : ( 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 where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A16, RCOMP_1:def_1; then ex x being Real st ( x = D2 . j & lower_bound A <= x & x <= upper_bound A ) ; then D2 . j in { r where r is Real : ( 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 divset (D2,j) c= divset (D1,i) by A12, A15, A17, XXREAL_2:def_12; ::_thesis: verum end; supposeA18: j <> 1 ; ::_thesis: divset (D2,j) c= divset (D1,i) A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; then A19: A = { r where r is Real : ( 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 where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A19; then ex x being Real st ( x = D2 . j & lower_bound A <= x & x <= upper_bound A ) ; then D2 . j in { r where r is Real : ( 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 where r is Real : ( 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 where r is Real : ( lower_bound A <= r & r <= upper_bound A ) } by A21, A22; then A24: ex x being Real 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 where r is Real : ( 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 divset (D2,j) c= divset (D1,i) by A12, A25, A20, XXREAL_2:def_12; ::_thesis: verum end; end; end; hence divset (D2,j) c= divset (D1,i) ; ::_thesis: verum end; supposeA26: i <> 1 ; ::_thesis: divset (D2,j) c= divset (D1,i) A27: j <> 1 proof assume A28: j = 1 ; ::_thesis: contradiction 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; ::_thesis: verum 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) ; ::_thesis: contradiction 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 ; ::_thesis: verum 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 where r is Real : ( 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 where r is Real : ( 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 divset (D2,j) c= divset (D1,i) by A48, A46, A47, XXREAL_2:def_12; ::_thesis: verum end; end; end; hence divset (D2,j) c= divset (D1,i) ; ::_thesis: verum end; hence ( i in dom D1 & divset (D2,j) c= divset (D1,i) ) by A9; ::_thesis: verum end; theorem :: INTEGRA2:38 for A, B being non empty closed_interval Subset of REAL st A c= B holds vol A <= vol B proof let A, B be non empty closed_interval Subset of REAL; ::_thesis: ( A c= B implies vol A <= vol B ) assume A1: A c= B ; ::_thesis: vol A <= vol 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 vol A <= vol B by INTEGRA1:def_5; ::_thesis: verum end; theorem :: INTEGRA2:39 for A being Subset of REAL for 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; ::_thesis: for a, x being Real st x in a ** A holds ex b being Real st ( b in A & x = a * b ) let a, x be Real; ::_thesis: ( x in a ** A implies ex b being Real st ( b in A & x = a * b ) ) assume x in a ** A ; ::_thesis: ex b being Real st ( b in A & x = a * b ) 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 = b as Real by A1; take b ; ::_thesis: ( b in A & x = a * b ) x = a * b by A1, XXREAL_3:def_5; hence ( b in A & x = a * b ) by A1; ::_thesis: verum end; begin theorem :: INTEGRA2:40 for A being non empty ext-real-membered set holds 0 ** A = {0} proof let A be non empty ext-real-membered set ; ::_thesis: 0 ** A = {0} for e being set holds ( e in 0 ** A iff e = 0 ) proof let e be set ; ::_thesis: ( e in 0 ** A iff e = 0 ) consider r being ext-real number such that A1: r in A by MEMBERED:8; hereby ::_thesis: ( e = 0 implies e in 0 ** A ) assume e in 0 ** A ; ::_thesis: e = 0 then ex z being Element of ExtREAL st ( e = 0 * z & z in A ) by MEMBER_1:188; hence e = 0 ; ::_thesis: verum end; assume e = 0 ; ::_thesis: e in 0 ** A then e = 0 * r ; hence e in 0 ** A by A1, MEMBER_1:186; ::_thesis: verum end; hence 0 ** A = {0} by TARSKI:def_1; ::_thesis: verum end;