:: MESFUNC1 semantic presentation begin definition func INT- -> Subset of REAL means :Def1: :: MESFUNC1:def 1 for r being Real holds ( r in it iff ex k being Element of NAT st r = - k ); existence ex b1 being Subset of REAL st for r being Real holds ( r in b1 iff ex k being Element of NAT st r = - k ) proof defpred S1[ Element of REAL ] means ex k being Element of NAT st \$1 = - k; consider IT being Subset of REAL such that A1: for r being Element of REAL holds ( r in IT iff S1[r] ) from SUBSET_1:sch_3(); take IT ; ::_thesis: for r being Real holds ( r in IT iff ex k being Element of NAT st r = - k ) thus for r being Real holds ( r in IT iff ex k being Element of NAT st r = - k ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Subset of REAL st ( for r being Real holds ( r in b1 iff ex k being Element of NAT st r = - k ) ) & ( for r being Real holds ( r in b2 iff ex k being Element of NAT st r = - k ) ) holds b1 = b2 proof let D1, D2 be Subset of REAL; ::_thesis: ( ( for r being Real holds ( r in D1 iff ex k being Element of NAT st r = - k ) ) & ( for r being Real holds ( r in D2 iff ex k being Element of NAT st r = - k ) ) implies D1 = D2 ) assume that A2: for r being Real holds ( r in D1 iff ex k being Element of NAT st r = - k ) and A3: for r being Real holds ( r in D2 iff ex k being Element of NAT st r = - k ) ; ::_thesis: D1 = D2 for r being Real holds ( r in D1 iff r in D2 ) proof let r be Real; ::_thesis: ( r in D1 iff r in D2 ) thus ( r in D1 implies r in D2 ) ::_thesis: ( r in D2 implies r in D1 ) proof assume r in D1 ; ::_thesis: r in D2 then ex k being Element of NAT st r = - k by A2; hence r in D2 by A3; ::_thesis: verum end; assume r in D2 ; ::_thesis: r in D1 then ex k being Element of NAT st r = - k by A3; hence r in D1 by A2; ::_thesis: verum end; hence D1 = D2 by SUBSET_1:3; ::_thesis: verum end; correctness ; end; :: deftheorem Def1 defines INT- MESFUNC1:def_1_:_ for b1 being Subset of REAL holds ( b1 = INT- iff for r being Real holds ( r in b1 iff ex k being Element of NAT st r = - k ) ); Lm1: 0 = - 0 ; registration cluster INT- -> non empty ; coherence not INT- is empty by Def1, Lm1; end; theorem Th1: :: MESFUNC1:1 NAT , INT- are_equipotent proof defpred S1[ Element of NAT , set ] means \$2 = - \$1; A1: for x being Element of NAT ex y being Element of INT- st S1[x,y] proof let x be Element of NAT ; ::_thesis: ex y being Element of INT- st S1[x,y] - x in INT- by Def1; hence ex y being Element of INT- st S1[x,y] ; ::_thesis: verum end; consider f being Function of NAT,INT- such that A2: for x being Element of NAT holds S1[x,f . x] from FUNCT_2:sch_3(A1); A3: f in Funcs (NAT,INT-) by FUNCT_2:8; then A4: dom f = NAT by FUNCT_2:92; A5: for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A6: x1 in dom f and A7: x2 in dom f and A8: f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider x1 = x1 as Element of NAT by A3, A6, FUNCT_2:92; reconsider x2 = x2 as Element of NAT by A3, A7, FUNCT_2:92; ( f . x1 = - x1 & f . x2 = - x2 ) by A2; then - (- x1) = x2 by A8; hence x1 = x2 ; ::_thesis: verum end; A9: for y being set st y in INT- holds f " {y} <> {} proof let y be set ; ::_thesis: ( y in INT- implies f " {y} <> {} ) assume A10: y in INT- ; ::_thesis: f " {y} <> {} then reconsider y = y as Real ; consider k being Element of NAT such that A11: y = - k by A10, Def1; f . k = - k by A2; then f . k in {y} by A11, TARSKI:def_1; hence f " {y} <> {} by A4, FUNCT_1:def_7; ::_thesis: verum end; A12: f is one-to-one by A5, FUNCT_1:def_4; rng f = INT- by A9, FUNCT_2:41; hence NAT , INT- are_equipotent by A4, A12, WELLORD2:def_4; ::_thesis: verum end; theorem Th2: :: MESFUNC1:2 INT = INT- \/ NAT proof for x being set st x in INT holds x in INT- \/ NAT proof let x be set ; ::_thesis: ( x in INT implies x in INT- \/ NAT ) assume x in INT ; ::_thesis: x in INT- \/ NAT then consider k being Element of NAT such that A1: ( x = k or x = - k ) by INT_1:def_1; now__::_thesis:_x_in_INT-_\/_NAT percases ( x = k or x = - k ) by A1; suppose x = k ; ::_thesis: x in INT- \/ NAT hence x in INT- \/ NAT by XBOOLE_0:def_3; ::_thesis: verum end; suppose x = - k ; ::_thesis: x in INT- \/ NAT then x in INT- by Def1; hence x in INT- \/ NAT by XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence x in INT- \/ NAT ; ::_thesis: verum end; then A2: INT c= INT- \/ NAT by TARSKI:def_3; for x being set st x in INT- \/ NAT holds x in INT proof let x be set ; ::_thesis: ( x in INT- \/ NAT implies x in INT ) assume A3: x in INT- \/ NAT ; ::_thesis: x in INT now__::_thesis:_x_in_INT percases ( x in INT- or x in NAT ) by A3, XBOOLE_0:def_3; suppose x in INT- ; ::_thesis: x in INT then ex k being Element of NAT st x = - k by Def1; hence x in INT by INT_1:def_1; ::_thesis: verum end; suppose x in NAT ; ::_thesis: x in INT hence x in INT by INT_1:def_1; ::_thesis: verum end; end; end; hence x in INT ; ::_thesis: verum end; then INT- \/ NAT c= INT by TARSKI:def_3; hence INT = INT- \/ NAT by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th3: :: MESFUNC1:3 NAT , INT are_equipotent by Th1, Th2, CARD_2:77; definition let n be Nat; func RAT_with_denominator n -> Subset of RAT means :Def2: :: MESFUNC1:def 2 for q being Rational holds ( q in it iff ex i being Integer st q = i / n ); existence ex b1 being Subset of RAT st for q being Rational holds ( q in b1 iff ex i being Integer st q = i / n ) proof defpred S1[ Element of RAT ] means ex i being Integer st \$1 = i / n; consider X being Subset of RAT such that A1: for r being Element of RAT holds ( r in X iff S1[r] ) from SUBSET_1:sch_3(); A2: for q being Rational holds ( q in X iff ex i being Integer st q = i / n ) proof let q be Rational; ::_thesis: ( q in X iff ex i being Integer st q = i / n ) reconsider q = q as Element of RAT by RAT_1:def_2; ( q in X iff ex i being Integer st q = i / n ) by A1; hence ( q in X iff ex i being Integer st q = i / n ) ; ::_thesis: verum end; take X ; ::_thesis: for q being Rational holds ( q in X iff ex i being Integer st q = i / n ) thus for q being Rational holds ( q in X iff ex i being Integer st q = i / n ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Subset of RAT st ( for q being Rational holds ( q in b1 iff ex i being Integer st q = i / n ) ) & ( for q being Rational holds ( q in b2 iff ex i being Integer st q = i / n ) ) holds b1 = b2 proof let D1, D2 be Subset of RAT; ::_thesis: ( ( for q being Rational holds ( q in D1 iff ex i being Integer st q = i / n ) ) & ( for q being Rational holds ( q in D2 iff ex i being Integer st q = i / n ) ) implies D1 = D2 ) assume that A3: for q being Rational holds ( q in D1 iff ex i being Integer st q = i / n ) and A4: for q being Rational holds ( q in D2 iff ex i being Integer st q = i / n ) ; ::_thesis: D1 = D2 for q being Element of RAT holds ( q in D1 iff q in D2 ) proof let q be Element of RAT ; ::_thesis: ( q in D1 iff q in D2 ) thus ( q in D1 implies q in D2 ) ::_thesis: ( q in D2 implies q in D1 ) proof assume A5: q in D1 ; ::_thesis: q in D2 reconsider q = q as Rational ; ex i being Integer st q = i / n by A3, A5; hence q in D2 by A4; ::_thesis: verum end; assume A6: q in D2 ; ::_thesis: q in D1 reconsider q = q as Rational ; ex i being Integer st q = i / n by A4, A6; hence q in D1 by A3; ::_thesis: verum end; hence D1 = D2 by SUBSET_1:3; ::_thesis: verum end; end; :: deftheorem Def2 defines RAT_with_denominator MESFUNC1:def_2_:_ for n being Nat for b2 being Subset of RAT holds ( b2 = RAT_with_denominator n iff for q being Rational holds ( q in b2 iff ex i being Integer st q = i / n ) ); registration let n be Nat; cluster RAT_with_denominator (n + 1) -> non empty ; coherence not RAT_with_denominator (n + 1) is empty proof reconsider i1 = n + 1 as Integer ; reconsider q = 0 / i1 as Rational ; q in RAT_with_denominator (n + 1) by Def2; hence not RAT_with_denominator (n + 1) is empty ; ::_thesis: verum end; end; theorem Th4: :: MESFUNC1:4 for n being Nat holds INT , RAT_with_denominator (n + 1) are_equipotent proof let n be Nat; ::_thesis: INT , RAT_with_denominator (n + 1) are_equipotent defpred S1[ Element of INT , set ] means \$2 = \$1 / (n + 1); A1: for x being Element of INT ex y being Element of RAT_with_denominator (n + 1) st S1[x,y] proof let x be Element of INT ; ::_thesis: ex y being Element of RAT_with_denominator (n + 1) st S1[x,y] reconsider x = x as Integer ; reconsider i1 = n + 1 as Integer ; set y = x / i1; x / i1 in RAT by RAT_1:def_1; then reconsider y = x / i1 as Rational ; y in RAT_with_denominator (n + 1) by Def2; hence ex y being Element of RAT_with_denominator (n + 1) st S1[x,y] ; ::_thesis: verum end; consider f being Function of INT,(RAT_with_denominator (n + 1)) such that A2: for x being Element of INT holds S1[x,f . x] from FUNCT_2:sch_3(A1); A3: f in Funcs (INT,(RAT_with_denominator (n + 1))) by FUNCT_2:8; then A4: dom f = INT by FUNCT_2:92; A5: for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 ) assume that A6: x1 in dom f and A7: x2 in dom f and A8: f . x1 = f . x2 ; ::_thesis: x1 = x2 reconsider x1 = x1 as Element of INT by A3, A6, FUNCT_2:92; reconsider x2 = x2 as Element of INT by A3, A7, FUNCT_2:92; ( f . x1 = x1 / (n + 1) & f . x2 = x2 / (n + 1) ) by A2; hence x1 = x2 by A8, XCMPLX_1:53; ::_thesis: verum end; A9: for y being set st y in RAT_with_denominator (n + 1) holds f " {y} <> {} proof let y be set ; ::_thesis: ( y in RAT_with_denominator (n + 1) implies f " {y} <> {} ) assume A10: y in RAT_with_denominator (n + 1) ; ::_thesis: f " {y} <> {} then reconsider y = y as Rational ; consider i being Integer such that A11: y = i / (n + 1) by A10, Def2; reconsider i = i as Element of INT by INT_1:def_2; f . i = i / (n + 1) by A2; then f . i in {y} by A11, TARSKI:def_1; hence f " {y} <> {} by A4, FUNCT_1:def_7; ::_thesis: verum end; A12: f is one-to-one by A5, FUNCT_1:def_4; rng f = RAT_with_denominator (n + 1) by A9, FUNCT_2:41; hence INT , RAT_with_denominator (n + 1) are_equipotent by A4, A12, WELLORD2:def_4; ::_thesis: verum end; theorem :: MESFUNC1:5 NAT , RAT are_equipotent proof assume A1: not NAT , RAT are_equipotent ; ::_thesis: contradiction defpred S1[ Element of NAT , Subset of REAL] means \$2 = RAT_with_denominator (\$1 + 1); A2: for n being Element of NAT ex X being Subset of REAL st S1[n,X] proof let n be Element of NAT ; ::_thesis: ex X being Subset of REAL st S1[n,X] for x being set st x in RAT_with_denominator (n + 1) holds x in REAL by NUMBERS:12, TARSKI:def_3; then reconsider X = RAT_with_denominator (n + 1) as Subset of REAL by TARSKI:def_3; take X ; ::_thesis: S1[n,X] thus S1[n,X] ; ::_thesis: verum end; consider F being Function of NAT,(bool REAL) such that A3: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A2); for x being set st x in union (rng F) holds x in RAT proof let x be set ; ::_thesis: ( x in union (rng F) implies x in RAT ) assume x in union (rng F) ; ::_thesis: x in RAT then consider Y being set such that A4: x in Y and A5: Y in rng F by TARSKI:def_4; dom F = NAT by FUNCT_2:def_1; then consider n being set such that A6: n in NAT and A7: F . n = Y by A5, FUNCT_1:def_3; reconsider n = n as Element of NAT by A6; Y = RAT_with_denominator (n + 1) by A3, A7; hence x in RAT by A4; ::_thesis: verum end; then A8: union (rng F) c= RAT by TARSKI:def_3; for x being set st x in RAT holds x in union (rng F) proof let x be set ; ::_thesis: ( x in RAT implies x in union (rng F) ) assume x in RAT ; ::_thesis: x in union (rng F) then reconsider x = x as Rational ; A9: dom F = NAT by FUNCT_2:def_1; denominator x <> 0 by RAT_1:def_3; then consider m being Nat such that A10: denominator x = m + 1 by NAT_1:6; reconsider m = m as Element of NAT by ORDINAL1:def_12; denominator x = m + 1 by A10; then reconsider n = (denominator x) - 1 as Element of NAT ; x = (numerator x) / (n + 1) by RAT_1:15; then x in RAT_with_denominator (n + 1) by Def2; then A11: x in F . n by A3; F . n in rng F by A9, FUNCT_1:def_3; hence x in union (rng F) by A11, TARSKI:def_4; ::_thesis: verum end; then RAT c= union (rng F) by TARSKI:def_3; then A12: union (rng F) = RAT by A8, XBOOLE_0:def_10; dom F = NAT by FUNCT_2:def_1; then A13: rng F is countable by CARD_3:93; for Y being set st Y in rng F holds Y is countable proof let Y be set ; ::_thesis: ( Y in rng F implies Y is countable ) assume Y in rng F ; ::_thesis: Y is countable then consider n being set such that A14: n in dom F and A15: F . n = Y by FUNCT_1:def_3; reconsider n = n as Element of NAT by A14, FUNCT_2:def_1; Y = RAT_with_denominator (n + 1) by A3, A15; then INT ,Y are_equipotent by Th4; then NAT ,Y are_equipotent by Th3, WELLORD2:15; then A16: card NAT = card Y by CARD_1:5; card NAT c= omega by CARD_3:def_14, CARD_4:2; hence Y is countable by A16, CARD_3:def_14; ::_thesis: verum end; then RAT is countable by A12, A13, CARD_4:12; then card RAT c= omega by CARD_3:def_14; then not omega in card RAT ; then ( not omega c= card RAT or not omega <> card RAT ) by CARD_1:3; then card RAT in omega by A1, CARD_1:4, CARD_1:5, CARD_1:47; hence contradiction ; ::_thesis: verum end; begin definition let C be non empty set ; let f1, f2 be C -defined ExtREAL -valued Function; deffunc H1( Element of C) -> Element of ExtREAL = (f1 . \$1) + (f2 . \$1); funcf1 + f2 -> PartFunc of C,ExtREAL means :: MESFUNC1:def 3 ( dom it = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom it holds it . c = (f1 . c) + (f2 . c) ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds b1 . c = (f1 . c) + (f2 . c) ) ) proof defpred S1[ Element of C] means \$1 in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))); consider F being PartFunc of C,ExtREAL such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F . c = H1(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom F holds F . c = (f1 . c) + (f2 . c) ) ) for x being set st x in dom F holds x in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) proof let x be set ; ::_thesis: ( x in dom F implies x in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) ) assume A3: x in dom F ; ::_thesis: x in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) dom F c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A3; x in dom F by A3; hence x in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) by A1; ::_thesis: verum end; then A4: dom F c= ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) by TARSKI:def_3; for x being set st x in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) holds x in dom F proof let x be set ; ::_thesis: ( x in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) implies x in dom F ) assume A5: x in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) ; ::_thesis: x in dom F then A6: x in dom f1 by XBOOLE_0:def_4; dom f1 c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A6; x in ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) by A5; hence x in dom F by A1; ::_thesis: verum end; then ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) c= dom F by TARSKI:def_3; hence dom F = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) by A4, XBOOLE_0:def_10; ::_thesis: for c being Element of C st c in dom F holds F . c = (f1 . c) + (f2 . c) let c be Element of C; ::_thesis: ( c in dom F implies F . c = (f1 . c) + (f2 . c) ) assume c in dom F ; ::_thesis: F . c = (f1 . c) + (f2 . c) hence F . c = (f1 . c) + (f2 . c) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds b1 . c = (f1 . c) + (f2 . c) ) & dom b2 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b2 holds b2 . c = (f1 . c) + (f2 . c) ) holds b1 = b2 proof set X = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))); thus for f, g being PartFunc of C,ExtREAL st dom f = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom f holds f . c = H1(c) ) & dom g = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom g holds g . c = H1(c) ) holds f = g from SEQ_1:sch_4(); ::_thesis: verum end; commutativity for b1 being PartFunc of C,ExtREAL for f1, f2 being C -defined ExtREAL -valued Function st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds b1 . c = (f1 . c) + (f2 . c) ) holds ( dom b1 = ((dom f2) /\ (dom f1)) \ (((f2 " {-infty}) /\ (f1 " {+infty})) \/ ((f2 " {+infty}) /\ (f1 " {-infty}))) & ( for c being Element of C st c in dom b1 holds b1 . c = (f2 . c) + (f1 . c) ) ) ; deffunc H2( Element of C) -> Element of ExtREAL = (f1 . \$1) - (f2 . \$1); funcf1 - f2 -> PartFunc of C,ExtREAL means :: MESFUNC1:def 4 ( dom it = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom it holds it . c = (f1 . c) - (f2 . c) ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds b1 . c = (f1 . c) - (f2 . c) ) ) proof defpred S1[ Element of C] means \$1 in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))); consider F being PartFunc of C,ExtREAL such that A7: for c being Element of C holds ( c in dom F iff S1[c] ) and A8: for c being Element of C st c in dom F holds F . c = H2(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom F holds F . c = (f1 . c) - (f2 . c) ) ) for x being set st x in dom F holds x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) proof let x be set ; ::_thesis: ( x in dom F implies x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) ) assume A9: x in dom F ; ::_thesis: x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) dom F c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A9; x in dom F by A9; hence x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by A7; ::_thesis: verum end; then A10: dom F c= ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by TARSKI:def_3; for x being set st x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) holds x in dom F proof let x be set ; ::_thesis: ( x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) implies x in dom F ) assume A11: x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) ; ::_thesis: x in dom F then A12: x in dom f1 by XBOOLE_0:def_4; dom f1 c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A12; x in ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by A11; hence x in dom F by A7; ::_thesis: verum end; then ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) c= dom F by TARSKI:def_3; hence dom F = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) by A10, XBOOLE_0:def_10; ::_thesis: for c being Element of C st c in dom F holds F . c = (f1 . c) - (f2 . c) let c be Element of C; ::_thesis: ( c in dom F implies F . c = (f1 . c) - (f2 . c) ) assume c in dom F ; ::_thesis: F . c = (f1 . c) - (f2 . c) hence F . c = (f1 . c) - (f2 . c) by A8; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b1 holds b1 . c = (f1 . c) - (f2 . c) ) & dom b2 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b2 holds b2 . c = (f1 . c) - (f2 . c) ) holds b1 = b2 proof set X = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))); thus for f, g being PartFunc of C,ExtREAL st dom f = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom f holds f . c = H2(c) ) & dom g = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom g holds g . c = H2(c) ) holds f = g from SEQ_1:sch_4(); ::_thesis: verum end; deffunc H3( Element of C) -> Element of ExtREAL = (f1 . \$1) * (f2 . \$1); funcf1 (#) f2 -> PartFunc of C,ExtREAL means :: MESFUNC1:def 5 ( dom it = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom it holds it . c = (f1 . c) * (f2 . c) ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 . c = (f1 . c) * (f2 . c) ) ) proof defpred S1[ Element of C] means \$1 in (dom f1) /\ (dom f2); consider F being PartFunc of C,ExtREAL such that A13: for c being Element of C holds ( c in dom F iff S1[c] ) and A14: for c being Element of C st c in dom F holds F . c = H3(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds F . c = (f1 . c) * (f2 . c) ) ) for x being set st x in dom F holds x in (dom f1) /\ (dom f2) proof let x be set ; ::_thesis: ( x in dom F implies x in (dom f1) /\ (dom f2) ) assume A15: x in dom F ; ::_thesis: x in (dom f1) /\ (dom f2) dom F c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A15; x in dom F by A15; hence x in (dom f1) /\ (dom f2) by A13; ::_thesis: verum end; then A16: dom F c= (dom f1) /\ (dom f2) by TARSKI:def_3; for x being set st x in (dom f1) /\ (dom f2) holds x in dom F proof let x be set ; ::_thesis: ( x in (dom f1) /\ (dom f2) implies x in dom F ) assume A17: x in (dom f1) /\ (dom f2) ; ::_thesis: x in dom F then A18: x in dom f1 by XBOOLE_0:def_4; dom f1 c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A18; x in (dom f1) /\ (dom f2) by A17; hence x in dom F by A13; ::_thesis: verum end; then (dom f1) /\ (dom f2) c= dom F by TARSKI:def_3; hence dom F = (dom f1) /\ (dom f2) by A16, XBOOLE_0:def_10; ::_thesis: for c being Element of C st c in dom F holds F . c = (f1 . c) * (f2 . c) let c be Element of C; ::_thesis: ( c in dom F implies F . c = (f1 . c) * (f2 . c) ) assume c in dom F ; ::_thesis: F . c = (f1 . c) * (f2 . c) hence F . c = (f1 . c) * (f2 . c) by A14; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 . c = (f1 . c) * (f2 . c) ) & dom b2 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b2 holds b2 . c = (f1 . c) * (f2 . c) ) holds b1 = b2 proof set X = (dom f1) /\ (dom f2); thus for F, G being PartFunc of C,ExtREAL st dom F = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom F holds F . c = H3(c) ) & dom G = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom G holds G . c = H3(c) ) holds F = G from SEQ_1:sch_4(); ::_thesis: verum end; commutativity for b1 being PartFunc of C,ExtREAL for f1, f2 being C -defined ExtREAL -valued Function st dom b1 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b1 holds b1 . c = (f1 . c) * (f2 . c) ) holds ( dom b1 = (dom f2) /\ (dom f1) & ( for c being Element of C st c in dom b1 holds b1 . c = (f2 . c) * (f1 . c) ) ) ; end; :: deftheorem defines + MESFUNC1:def_3_:_ for C being non empty set for f1, f2 being b1 -defined ExtREAL -valued Function for b4 being PartFunc of C,ExtREAL holds ( b4 = f1 + f2 iff ( dom b4 = ((dom f1) /\ (dom f2)) \ (((f1 " {-infty}) /\ (f2 " {+infty})) \/ ((f1 " {+infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b4 holds b4 . c = (f1 . c) + (f2 . c) ) ) ); :: deftheorem defines - MESFUNC1:def_4_:_ for C being non empty set for f1, f2 being b1 -defined ExtREAL -valued Function for b4 being PartFunc of C,ExtREAL holds ( b4 = f1 - f2 iff ( dom b4 = ((dom f1) /\ (dom f2)) \ (((f1 " {+infty}) /\ (f2 " {+infty})) \/ ((f1 " {-infty}) /\ (f2 " {-infty}))) & ( for c being Element of C st c in dom b4 holds b4 . c = (f1 . c) - (f2 . c) ) ) ); :: deftheorem defines (#) MESFUNC1:def_5_:_ for C being non empty set for f1, f2 being b1 -defined ExtREAL -valued Function for b4 being PartFunc of C,ExtREAL holds ( b4 = f1 (#) f2 iff ( dom b4 = (dom f1) /\ (dom f2) & ( for c being Element of C st c in dom b4 holds b4 . c = (f1 . c) * (f2 . c) ) ) ); definition let C be non empty set ; let f be C -defined ExtREAL -valued Function; let r be Real; deffunc H1( Element of C) -> Element of ExtREAL = (R_EAL r) * (f . \$1); funcr (#) f -> PartFunc of C,ExtREAL means :Def6: :: MESFUNC1:def 6 ( dom it = dom f & ( for c being Element of C st c in dom it holds it . c = (R_EAL r) * (f . c) ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 . c = (R_EAL r) * (f . c) ) ) proof defpred S1[ Element of C] means \$1 in dom f; consider F being PartFunc of C,ExtREAL such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F . c = H1(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds F . c = (R_EAL r) * (f . c) ) ) for x being set st x in dom F holds x in dom f proof let x be set ; ::_thesis: ( x in dom F implies x in dom f ) assume A3: x in dom F ; ::_thesis: x in dom f dom F c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A3; x in dom F by A3; hence x in dom f by A1; ::_thesis: verum end; then A4: dom F c= dom f by TARSKI:def_3; for x being set st x in dom f holds x in dom F proof let x be set ; ::_thesis: ( x in dom f implies x in dom F ) assume A5: x in dom f ; ::_thesis: x in dom F dom f c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A5; x in dom f by A5; hence x in dom F by A1; ::_thesis: verum end; then dom f c= dom F by TARSKI:def_3; hence dom F = dom f by A4, XBOOLE_0:def_10; ::_thesis: for c being Element of C st c in dom F holds F . c = (R_EAL r) * (f . c) let c be Element of C; ::_thesis: ( c in dom F implies F . c = (R_EAL r) * (f . c) ) assume c in dom F ; ::_thesis: F . c = (R_EAL r) * (f . c) hence F . c = (R_EAL r) * (f . c) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 . c = (R_EAL r) * (f . c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds b2 . c = (R_EAL r) * (f . c) ) holds b1 = b2 proof set X = dom f; thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds F . c = H1(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds G . c = H1(c) ) holds F = G from SEQ_1:sch_4(); ::_thesis: verum end; end; :: deftheorem Def6 defines (#) MESFUNC1:def_6_:_ for C being non empty set for f being b1 -defined ExtREAL -valued Function for r being Real for b4 being PartFunc of C,ExtREAL holds ( b4 = r (#) f iff ( dom b4 = dom f & ( for c being Element of C st c in dom b4 holds b4 . c = (R_EAL r) * (f . c) ) ) ); theorem Th6: :: MESFUNC1:6 for C being non empty set for f being PartFunc of C,ExtREAL for r being Real st r <> 0 holds for c being Element of C st c in dom (r (#) f) holds f . c = ((r (#) f) . c) / (R_EAL r) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL for r being Real st r <> 0 holds for c being Element of C st c in dom (r (#) f) holds f . c = ((r (#) f) . c) / (R_EAL r) let f be PartFunc of C,ExtREAL; ::_thesis: for r being Real st r <> 0 holds for c being Element of C st c in dom (r (#) f) holds f . c = ((r (#) f) . c) / (R_EAL r) let r be Real; ::_thesis: ( r <> 0 implies for c being Element of C st c in dom (r (#) f) holds f . c = ((r (#) f) . c) / (R_EAL r) ) assume A1: r <> 0 ; ::_thesis: for c being Element of C st c in dom (r (#) f) holds f . c = ((r (#) f) . c) / (R_EAL r) let c be Element of C; ::_thesis: ( c in dom (r (#) f) implies f . c = ((r (#) f) . c) / (R_EAL r) ) assume c in dom (r (#) f) ; ::_thesis: f . c = ((r (#) f) . c) / (R_EAL r) then A2: (r (#) f) . c = (R_EAL r) * (f . c) by Def6; percases ( f . c = +infty or f . c = -infty or ( f . c <> +infty & f . c <> -infty ) ) ; supposeA3: f . c = +infty ; ::_thesis: f . c = ((r (#) f) . c) / (R_EAL r) now__::_thesis:_f_._c_=_((r_(#)_f)_._c)_/_(R_EAL_r) percases ( 0. < R_EAL r or R_EAL r < 0. ) by A1; supposeA4: 0. < R_EAL r ; ::_thesis: f . c = ((r (#) f) . c) / (R_EAL r) then (r (#) f) . c = +infty by A2, A3, XXREAL_3:def_5; hence f . c = ((r (#) f) . c) / (R_EAL r) by A3, A4, XXREAL_3:83; ::_thesis: verum end; supposeA5: R_EAL r < 0. ; ::_thesis: f . c = ((r (#) f) . c) / (R_EAL r) then (r (#) f) . c = -infty by A2, A3, XXREAL_3:def_5; hence f . c = ((r (#) f) . c) / (R_EAL r) by A3, A5, XXREAL_3:84; ::_thesis: verum end; end; end; hence f . c = ((r (#) f) . c) / (R_EAL r) ; ::_thesis: verum end; supposeA6: f . c = -infty ; ::_thesis: f . c = ((r (#) f) . c) / (R_EAL r) now__::_thesis:_f_._c_=_((r_(#)_f)_._c)_/_(R_EAL_r) percases ( 0. < R_EAL r or R_EAL r < 0. ) by A1; supposeA7: 0. < R_EAL r ; ::_thesis: f . c = ((r (#) f) . c) / (R_EAL r) then (r (#) f) . c = -infty by A2, A6, XXREAL_3:def_5; hence f . c = ((r (#) f) . c) / (R_EAL r) by A6, A7, XXREAL_3:86; ::_thesis: verum end; supposeA8: R_EAL r < 0. ; ::_thesis: f . c = ((r (#) f) . c) / (R_EAL r) then (r (#) f) . c = +infty by A2, A6, XXREAL_3:def_5; hence f . c = ((r (#) f) . c) / (R_EAL r) by A6, A8, XXREAL_3:85; ::_thesis: verum end; end; end; hence f . c = ((r (#) f) . c) / (R_EAL r) ; ::_thesis: verum end; suppose ( f . c <> +infty & f . c <> -infty ) ; ::_thesis: f . c = ((r (#) f) . c) / (R_EAL r) then reconsider a = f . c as Real by XXREAL_0:14; (r (#) f) . c = r * a by A2, EXTREAL1:1; then ((r (#) f) . c) / (R_EAL r) = (r * a) / r by EXTREAL1:2 .= a / (r / r) by XCMPLX_1:77 .= a / 1 by A1, XCMPLX_1:60 ; hence f . c = ((r (#) f) . c) / (R_EAL r) ; ::_thesis: verum end; end; end; definition let C be non empty set ; let f be C -defined ExtREAL -valued Function; deffunc H1( Element of C) -> Element of ExtREAL = - (f . \$1); func - f -> PartFunc of C,ExtREAL means :: MESFUNC1:def 7 ( dom it = dom f & ( for c being Element of C st c in dom it holds it . c = - (f . c) ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 . c = - (f . c) ) ) proof defpred S1[ Element of C] means \$1 in dom f; consider F being PartFunc of C,ExtREAL such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F . c = H1(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds F . c = - (f . c) ) ) for x being set st x in dom F holds x in dom f proof let x be set ; ::_thesis: ( x in dom F implies x in dom f ) assume A3: x in dom F ; ::_thesis: x in dom f dom F c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A3; x in dom F by A3; hence x in dom f by A1; ::_thesis: verum end; then A4: dom F c= dom f by TARSKI:def_3; for x being set st x in dom f holds x in dom F proof let x be set ; ::_thesis: ( x in dom f implies x in dom F ) assume A5: x in dom f ; ::_thesis: x in dom F dom f c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A5; x in dom f by A5; hence x in dom F by A1; ::_thesis: verum end; then dom f c= dom F by TARSKI:def_3; hence dom F = dom f by A4, XBOOLE_0:def_10; ::_thesis: for c being Element of C st c in dom F holds F . c = - (f . c) let c be Element of C; ::_thesis: ( c in dom F implies F . c = - (f . c) ) assume c in dom F ; ::_thesis: F . c = - (f . c) hence F . c = - (f . c) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 . c = - (f . c) ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds b2 . c = - (f . c) ) holds b1 = b2 proof set X = dom f; thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds F . c = H1(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds G . c = H1(c) ) holds F = G from SEQ_1:sch_4(); ::_thesis: verum end; end; :: deftheorem defines - MESFUNC1:def_7_:_ for C being non empty set for f being b1 -defined ExtREAL -valued Function for b3 being PartFunc of C,ExtREAL holds ( b3 = - f iff ( dom b3 = dom f & ( for c being Element of C st c in dom b3 holds b3 . c = - (f . c) ) ) ); definition func 1. -> R_eal equals :: MESFUNC1:def 8 1; correctness coherence 1 is R_eal; by XXREAL_0:def_1; end; :: deftheorem defines 1. MESFUNC1:def_8_:_ 1. = 1; definition let C be non empty set ; let f be C -defined ExtREAL -valued Function; let r be Real; deffunc H1( Element of C) -> Element of ExtREAL = (R_EAL r) / (f . \$1); funcr / f -> PartFunc of C,ExtREAL means :Def9: :: MESFUNC1:def 9 ( dom it = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom it holds it . c = (R_EAL r) / (f . c) ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b1 holds b1 . c = (R_EAL r) / (f . c) ) ) proof defpred S1[ Element of C] means \$1 in (dom f) \ (f " {0.}); consider F being PartFunc of C,ExtREAL such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F . c = H1(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom F holds F . c = (R_EAL r) / (f . c) ) ) for x being set st x in dom F holds x in (dom f) \ (f " {0.}) proof let x be set ; ::_thesis: ( x in dom F implies x in (dom f) \ (f " {0.}) ) assume A3: x in dom F ; ::_thesis: x in (dom f) \ (f " {0.}) dom F c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A3; x in dom F by A3; hence x in (dom f) \ (f " {0.}) by A1; ::_thesis: verum end; then A4: dom F c= (dom f) \ (f " {0.}) by TARSKI:def_3; for x being set st x in (dom f) \ (f " {0.}) holds x in dom F proof let x be set ; ::_thesis: ( x in (dom f) \ (f " {0.}) implies x in dom F ) assume A5: x in (dom f) \ (f " {0.}) ; ::_thesis: x in dom F dom f c= C by RELAT_1:def_18; then (dom f) \ (f " {0.}) c= C by XBOOLE_1:1; then reconsider x = x as Element of C by A5; x in (dom f) \ (f " {0.}) by A5; hence x in dom F by A1; ::_thesis: verum end; then (dom f) \ (f " {0.}) c= dom F by TARSKI:def_3; hence dom F = (dom f) \ (f " {0.}) by A4, XBOOLE_0:def_10; ::_thesis: for c being Element of C st c in dom F holds F . c = (R_EAL r) / (f . c) let c be Element of C; ::_thesis: ( c in dom F implies F . c = (R_EAL r) / (f . c) ) assume c in dom F ; ::_thesis: F . c = (R_EAL r) / (f . c) hence F . c = (R_EAL r) / (f . c) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b1 holds b1 . c = (R_EAL r) / (f . c) ) & dom b2 = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b2 holds b2 . c = (R_EAL r) / (f . c) ) holds b1 = b2 proof set X = (dom f) \ (f " {0.}); thus for F, G being PartFunc of C,ExtREAL st dom F = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom F holds F . c = H1(c) ) & dom G = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom G holds G . c = H1(c) ) holds F = G from SEQ_1:sch_4(); ::_thesis: verum end; end; :: deftheorem Def9 defines / MESFUNC1:def_9_:_ for C being non empty set for f being b1 -defined ExtREAL -valued Function for r being Real for b4 being PartFunc of C,ExtREAL holds ( b4 = r / f iff ( dom b4 = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom b4 holds b4 . c = (R_EAL r) / (f . c) ) ) ); theorem :: MESFUNC1:7 for C being non empty set for f being PartFunc of C,ExtREAL holds ( dom (1 / f) = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom (1 / f) holds (1 / f) . c = 1. / (f . c) ) ) proof let C be non empty set ; ::_thesis: for f being PartFunc of C,ExtREAL holds ( dom (1 / f) = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom (1 / f) holds (1 / f) . c = 1. / (f . c) ) ) let f be PartFunc of C,ExtREAL; ::_thesis: ( dom (1 / f) = (dom f) \ (f " {0.}) & ( for c being Element of C st c in dom (1 / f) holds (1 / f) . c = 1. / (f . c) ) ) thus dom (1 / f) = (dom f) \ (f " {0.}) by Def9; ::_thesis: for c being Element of C st c in dom (1 / f) holds (1 / f) . c = 1. / (f . c) thus for c being Element of C st c in dom (1 / f) holds (1 / f) . c = 1. / (f . c) ::_thesis: verum proof let c be Element of C; ::_thesis: ( c in dom (1 / f) implies (1 / f) . c = 1. / (f . c) ) assume c in dom (1 / f) ; ::_thesis: (1 / f) . c = 1. / (f . c) then (1 / f) . c = (R_EAL 1) / (f . c) by Def9; hence (1 / f) . c = 1. / (f . c) ; ::_thesis: verum end; end; definition let C be non empty set ; let f be C -defined ExtREAL -valued Function; deffunc H1( Element of C) -> Element of ExtREAL = |.(f . \$1).|; func|.f.| -> PartFunc of C,ExtREAL means :: MESFUNC1:def 10 ( dom it = dom f & ( for c being Element of C st c in dom it holds it . c = |.(f . c).| ) ); existence ex b1 being PartFunc of C,ExtREAL st ( dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 . c = |.(f . c).| ) ) proof defpred S1[ Element of C] means \$1 in dom f; consider F being PartFunc of C,ExtREAL such that A1: for c being Element of C holds ( c in dom F iff S1[c] ) and A2: for c being Element of C st c in dom F holds F . c = H1(c) from SEQ_1:sch_3(); take F ; ::_thesis: ( dom F = dom f & ( for c being Element of C st c in dom F holds F . c = |.(f . c).| ) ) for x being set st x in dom F holds x in dom f proof let x be set ; ::_thesis: ( x in dom F implies x in dom f ) assume A3: x in dom F ; ::_thesis: x in dom f dom F c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A3; x in dom F by A3; hence x in dom f by A1; ::_thesis: verum end; then A4: dom F c= dom f by TARSKI:def_3; for x being set st x in dom f holds x in dom F proof let x be set ; ::_thesis: ( x in dom f implies x in dom F ) assume A5: x in dom f ; ::_thesis: x in dom F dom f c= C by RELAT_1:def_18; then reconsider x = x as Element of C by A5; x in dom f by A5; hence x in dom F by A1; ::_thesis: verum end; then dom f c= dom F by TARSKI:def_3; hence dom F = dom f by A4, XBOOLE_0:def_10; ::_thesis: for c being Element of C st c in dom F holds F . c = |.(f . c).| let c be Element of C; ::_thesis: ( c in dom F implies F . c = |.(f . c).| ) assume c in dom F ; ::_thesis: F . c = |.(f . c).| hence F . c = |.(f . c).| by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of C,ExtREAL st dom b1 = dom f & ( for c being Element of C st c in dom b1 holds b1 . c = |.(f . c).| ) & dom b2 = dom f & ( for c being Element of C st c in dom b2 holds b2 . c = |.(f . c).| ) holds b1 = b2 proof set X = dom f; thus for F, G being PartFunc of C,ExtREAL st dom F = dom f & ( for c being Element of C st c in dom F holds F . c = H1(c) ) & dom G = dom f & ( for c being Element of C st c in dom G holds G . c = H1(c) ) holds F = G from SEQ_1:sch_4(); ::_thesis: verum end; end; :: deftheorem defines |. MESFUNC1:def_10_:_ for C being non empty set for f being b1 -defined ExtREAL -valued Function for b3 being PartFunc of C,ExtREAL holds ( b3 = |.f.| iff ( dom b3 = dom f & ( for c being Element of C st c in dom b3 holds b3 . c = |.(f . c).| ) ) ); begin theorem Th8: :: MESFUNC1:8 for r being Real ex n being Element of NAT st r <= n proof let r be Real; ::_thesis: ex n being Element of NAT st r <= n percases ( [/r\] >= 0 or [/r\] < 0 ) ; suppose [/r\] >= 0 ; ::_thesis: ex n being Element of NAT st r <= n then reconsider n = [/r\] as Element of NAT by INT_1:3; take n ; ::_thesis: r <= n thus r <= n by INT_1:def_7; ::_thesis: verum end; supposeA1: [/r\] < 0 ; ::_thesis: ex n being Element of NAT st r <= n take 0 ; ::_thesis: r <= 0 thus r <= 0 by A1, INT_1:def_7; ::_thesis: verum end; end; end; theorem Th9: :: MESFUNC1:9 for r being Real ex n being Element of NAT st - n <= r proof let r be Real; ::_thesis: ex n being Element of NAT st - n <= r [\r/] is Element of INT by INT_1:def_2; then A1: ( [\r/] <= r & ex k being Element of NAT st ( [\r/] = k or [\r/] = - k ) ) by INT_1:def_1, INT_1:def_6; percases ( [\r/] < 0 or [\r/] >= 0 ) ; suppose [\r/] < 0 ; ::_thesis: ex n being Element of NAT st - n <= r hence ex n being Element of NAT st - n <= r by A1; ::_thesis: verum end; supposeA2: [\r/] >= 0 ; ::_thesis: ex n being Element of NAT st - n <= r take 0 ; ::_thesis: - 0 <= r thus - 0 <= r by A2, INT_1:def_6; ::_thesis: verum end; end; end; theorem Th10: :: MESFUNC1:10 for r, s being real number st r < s holds ex n being Element of NAT st 1 / (n + 1) < s - r proof let r, s be real number ; ::_thesis: ( r < s implies ex n being Element of NAT st 1 / (n + 1) < s - r ) assume r < s ; ::_thesis: ex n being Element of NAT st 1 / (n + 1) < s - r then s - r > 0 by XREAL_1:50; then consider t being real number such that A1: 0 < t and A2: t < s - r by XREAL_1:5; reconsider t = t as Real by XREAL_0:def_1; A3: 1 / t > 0 by A1, XREAL_1:139; A4: [/(1 / t)\] + 1 > 1 / t by INT_1:32; set n = [/(1 / t)\]; reconsider n = [/(1 / t)\] as Element of NAT by A3, A4, INT_1:3, INT_1:7; (n + 1) * t >= 1 by A1, A4, XREAL_1:81; then 1 / (n + 1) <= t by XREAL_1:79; then 1 / (n + 1) < s - r by A2, XXREAL_0:2; hence ex n being Element of NAT st 1 / (n + 1) < s - r ; ::_thesis: verum end; theorem Th11: :: MESFUNC1:11 for r, s being real number st ( for n being Element of NAT holds r - (1 / (n + 1)) <= s ) holds r <= s proof let r, s be real number ; ::_thesis: ( ( for n being Element of NAT holds r - (1 / (n + 1)) <= s ) implies r <= s ) assume A1: for n being Element of NAT holds r - (1 / (n + 1)) <= s ; ::_thesis: r <= s assume r > s ; ::_thesis: contradiction then consider n being Element of NAT such that A2: 1 / (n + 1) < r - s by Th10; s + (1 / (n + 1)) < r by A2, XREAL_1:20; then s < r - (1 / (n + 1)) by XREAL_1:20; hence contradiction by A1; ::_thesis: verum end; theorem Th12: :: MESFUNC1:12 for a being R_eal st ( for r being Real holds R_EAL r < a ) holds a = +infty proof let a be R_eal; ::_thesis: ( ( for r being Real holds R_EAL r < a ) implies a = +infty ) assume A1: for r being Real holds R_EAL r < a ; ::_thesis: a = +infty assume not a = +infty ; ::_thesis: contradiction then a < +infty by XXREAL_0:4; then consider b being R_eal such that A2: a < b and b < +infty and A3: b in REAL by MEASURE5:2; reconsider b = b as Real by A3; a <= R_EAL b by A2; hence contradiction by A1; ::_thesis: verum end; theorem Th13: :: MESFUNC1:13 for a being R_eal st ( for r being Real holds a < R_EAL r ) holds a = -infty proof let a be R_eal; ::_thesis: ( ( for r being Real holds a < R_EAL r ) implies a = -infty ) assume A1: for r being Real holds a < R_EAL r ; ::_thesis: a = -infty assume A2: not a = -infty ; ::_thesis: contradiction -infty <= a by XXREAL_0:5; then -infty < a by A2, XXREAL_0:1; then consider b being R_eal such that -infty < b and A3: b < a and A4: b in REAL by MEASURE5:2; reconsider b = b as Real by A4; R_EAL b <= a by A3; hence contradiction by A1; ::_thesis: verum end; notation let f be ext-real-valued Function; let a be ext-real number ; synonym eq_dom (f,a) for Coim (f,a); end; definition let f be ext-real-valued Function; let a be ext-real number ; defpred S1[ set ] means ( \$1 in dom f & f . \$1 < a ); func less_dom (f,a) -> set means :Def11: :: MESFUNC1:def 11 for x being set holds ( x in it iff ( x in dom f & f . x < a ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in dom f & f . x < a ) ) proof consider A being set such that A1: for x being set holds ( x in A iff ( x in dom f & S1[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for x being set holds ( x in A iff ( x in dom f & f . x < a ) ) thus for x being set holds ( x in A iff ( x in dom f & f . x < a ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in dom f & f . x < a ) ) ) & ( for x being set holds ( x in b2 iff ( x in dom f & f . x < a ) ) ) holds b1 = b2 proof thus for D1, D2 being set st ( for x being set holds ( x in D1 iff S1[x] ) ) & ( for x being set holds ( x in D2 iff S1[x] ) ) holds D1 = D2 from XBOOLE_0:sch_3(); ::_thesis: verum end; defpred S2[ set ] means ( \$1 in dom f & f . \$1 <= a ); func less_eq_dom (f,a) -> set means :Def12: :: MESFUNC1:def 12 for x being set holds ( x in it iff ( x in dom f & f . x <= a ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in dom f & f . x <= a ) ) proof consider A being set such that A2: for x being set holds ( x in A iff ( x in dom f & S2[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for x being set holds ( x in A iff ( x in dom f & f . x <= a ) ) thus for x being set holds ( x in A iff ( x in dom f & f . x <= a ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in dom f & f . x <= a ) ) ) & ( for x being set holds ( x in b2 iff ( x in dom f & f . x <= a ) ) ) holds b1 = b2 proof thus for D1, D2 being set st ( for x being set holds ( x in D1 iff S2[x] ) ) & ( for x being set holds ( x in D2 iff S2[x] ) ) holds D1 = D2 from XBOOLE_0:sch_3(); ::_thesis: verum end; defpred S3[ set ] means ( \$1 in dom f & a < f . \$1 ); func great_dom (f,a) -> set means :Def13: :: MESFUNC1:def 13 for x being set holds ( x in it iff ( x in dom f & a < f . x ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in dom f & a < f . x ) ) proof consider A being set such that A3: for x being set holds ( x in A iff ( x in dom f & S3[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for x being set holds ( x in A iff ( x in dom f & a < f . x ) ) thus for x being set holds ( x in A iff ( x in dom f & a < f . x ) ) by A3; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in dom f & a < f . x ) ) ) & ( for x being set holds ( x in b2 iff ( x in dom f & a < f . x ) ) ) holds b1 = b2 proof thus for D1, D2 being set st ( for x being set holds ( x in D1 iff S3[x] ) ) & ( for x being set holds ( x in D2 iff S3[x] ) ) holds D1 = D2 from XBOOLE_0:sch_3(); ::_thesis: verum end; defpred S4[ set ] means ( \$1 in dom f & a <= f . \$1 ); func great_eq_dom (f,a) -> set means :Def14: :: MESFUNC1:def 14 for x being set holds ( x in it iff ( x in dom f & a <= f . x ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x in dom f & a <= f . x ) ) proof consider A being set such that A4: for x being set holds ( x in A iff ( x in dom f & S4[x] ) ) from XBOOLE_0:sch_1(); take A ; ::_thesis: for x being set holds ( x in A iff ( x in dom f & a <= f . x ) ) thus for x being set holds ( x in A iff ( x in dom f & a <= f . x ) ) by A4; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x in dom f & a <= f . x ) ) ) & ( for x being set holds ( x in b2 iff ( x in dom f & a <= f . x ) ) ) holds b1 = b2 proof thus for D1, D2 being set st ( for x being set holds ( x in D1 iff S4[x] ) ) & ( for x being set holds ( x in D2 iff S4[x] ) ) holds D1 = D2 from XBOOLE_0:sch_3(); ::_thesis: verum end; redefine func Coim (f,a) means :Def15: :: MESFUNC1:def 15 for x being set holds ( x in it iff ( x in dom f & f . x = a ) ); compatibility for b1 being set holds ( b1 = eq_dom (f,a) iff for x being set holds ( x in b1 iff ( x in dom f & f . x = a ) ) ) proof let X be set ; ::_thesis: ( X = eq_dom (f,a) iff for x being set holds ( x in X iff ( x in dom f & f . x = a ) ) ) thus ( X = eq_dom (f,a) implies for x being set holds ( x in X iff ( x in dom f & f . x = a ) ) ) ::_thesis: ( ( for x being set holds ( x in X iff ( x in dom f & f . x = a ) ) ) implies X = eq_dom (f,a) ) proof assume A5: X = eq_dom (f,a) ; ::_thesis: for x being set holds ( x in X iff ( x in dom f & f . x = a ) ) let x be set ; ::_thesis: ( x in X iff ( x in dom f & f . x = a ) ) thus ( x in X implies ( x in dom f & f . x = a ) ) ::_thesis: ( x in dom f & f . x = a implies x in X ) proof assume A6: x in X ; ::_thesis: ( x in dom f & f . x = a ) hence x in dom f by A5, FUNCT_1:def_7; ::_thesis: f . x = a f . x in {a} by A5, A6, FUNCT_1:def_7; hence f . x = a by TARSKI:def_1; ::_thesis: verum end; assume A7: x in dom f ; ::_thesis: ( not f . x = a or x in X ) assume f . x = a ; ::_thesis: x in X then f . x in {a} by TARSKI:def_1; hence x in X by A5, A7, FUNCT_1:def_7; ::_thesis: verum end; assume A8: for x being set holds ( x in X iff ( x in dom f & f . x = a ) ) ; ::_thesis: X = eq_dom (f,a) for x being set holds ( x in X iff ( x in dom f & f . x in {a} ) ) proof let x be set ; ::_thesis: ( x in X iff ( x in dom f & f . x in {a} ) ) thus ( x in X implies ( x in dom f & f . x in {a} ) ) ::_thesis: ( x in dom f & f . x in {a} implies x in X ) proof assume A9: x in X ; ::_thesis: ( x in dom f & f . x in {a} ) hence x in dom f by A8; ::_thesis: f . x in {a} f . x = a by A8, A9; hence f . x in {a} by TARSKI:def_1; ::_thesis: verum end; assume A10: x in dom f ; ::_thesis: ( not f . x in {a} or x in X ) assume f . x in {a} ; ::_thesis: x in X then f . x = a by TARSKI:def_1; hence x in X by A8, A10; ::_thesis: verum end; hence X = eq_dom (f,a) by FUNCT_1:def_7; ::_thesis: verum end; end; :: deftheorem Def11 defines less_dom MESFUNC1:def_11_:_ for f being ext-real-valued Function for a being ext-real number for b3 being set holds ( b3 = less_dom (f,a) iff for x being set holds ( x in b3 iff ( x in dom f & f . x < a ) ) ); :: deftheorem Def12 defines less_eq_dom MESFUNC1:def_12_:_ for f being ext-real-valued Function for a being ext-real number for b3 being set holds ( b3 = less_eq_dom (f,a) iff for x being set holds ( x in b3 iff ( x in dom f & f . x <= a ) ) ); :: deftheorem Def13 defines great_dom MESFUNC1:def_13_:_ for f being ext-real-valued Function for a being ext-real number for b3 being set holds ( b3 = great_dom (f,a) iff for x being set holds ( x in b3 iff ( x in dom f & a < f . x ) ) ); :: deftheorem Def14 defines great_eq_dom MESFUNC1:def_14_:_ for f being ext-real-valued Function for a being ext-real number for b3 being set holds ( b3 = great_eq_dom (f,a) iff for x being set holds ( x in b3 iff ( x in dom f & a <= f . x ) ) ); :: deftheorem Def15 defines eq_dom MESFUNC1:def_15_:_ for f being ext-real-valued Function for a being ext-real number for b3 being set holds ( b3 = eq_dom (f,a) iff for x being set holds ( x in b3 iff ( x in dom f & f . x = a ) ) ); definition let X be set ; let f be PartFunc of X,ExtREAL; let a be ext-real number ; :: original: less_dom redefine func less_dom (f,a) -> Subset of X; coherence less_dom (f,a) is Subset of X proof less_dom (f,a) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in less_dom (f,a) or x in X ) assume x in less_dom (f,a) ; ::_thesis: x in X then A1: x in dom f by Def11; dom f c= X by RELAT_1:def_18; hence x in X by A1; ::_thesis: verum end; hence less_dom (f,a) is Subset of X ; ::_thesis: verum end; :: original: less_eq_dom redefine func less_eq_dom (f,a) -> Subset of X; coherence less_eq_dom (f,a) is Subset of X proof less_eq_dom (f,a) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in less_eq_dom (f,a) or x in X ) assume x in less_eq_dom (f,a) ; ::_thesis: x in X then A2: x in dom f by Def12; dom f c= X by RELAT_1:def_18; hence x in X by A2; ::_thesis: verum end; hence less_eq_dom (f,a) is Subset of X ; ::_thesis: verum end; :: original: great_dom redefine func great_dom (f,a) -> Subset of X; coherence great_dom (f,a) is Subset of X proof great_dom (f,a) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in great_dom (f,a) or x in X ) assume x in great_dom (f,a) ; ::_thesis: x in X then A3: x in dom f by Def13; dom f c= X by RELAT_1:def_18; hence x in X by A3; ::_thesis: verum end; hence great_dom (f,a) is Subset of X ; ::_thesis: verum end; :: original: great_eq_dom redefine func great_eq_dom (f,a) -> Subset of X; coherence great_eq_dom (f,a) is Subset of X proof great_eq_dom (f,a) c= X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in great_eq_dom (f,a) or x in X ) assume x in great_eq_dom (f,a) ; ::_thesis: x in X then A4: x in dom f by Def14; dom f c= X by RELAT_1:def_18; hence x in X by A4; ::_thesis: verum end; hence great_eq_dom (f,a) is Subset of X ; ::_thesis: verum end; :: original: eq_dom redefine func eq_dom (f,a) -> Subset of X; coherence eq_dom (f,a) is Subset of X proof Coim (f,a) is Subset of X ; hence eq_dom (f,a) is Subset of X ; ::_thesis: verum end; end; theorem Th14: :: MESFUNC1:14 for X being set for f being PartFunc of X,ExtREAL for A being set for a being R_eal st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) proof let X be set ; ::_thesis: for f being PartFunc of X,ExtREAL for A being set for a being R_eal st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set for a being R_eal st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) let A be set ; ::_thesis: for a being R_eal st A c= dom f holds A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) let a be R_eal; ::_thesis: ( A c= dom f implies A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) ) assume A1: A c= dom f ; ::_thesis: A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) dom f c= X by RELAT_1:def_18; then A2: A c= X by A1, XBOOLE_1:1; for x being set st x in A /\ (great_eq_dom (f,a)) holds x in A \ (A /\ (less_dom (f,a))) proof let x be set ; ::_thesis: ( x in A /\ (great_eq_dom (f,a)) implies x in A \ (A /\ (less_dom (f,a))) ) assume A3: x in A /\ (great_eq_dom (f,a)) ; ::_thesis: x in A \ (A /\ (less_dom (f,a))) then A4: x in A by XBOOLE_0:def_4; x in great_eq_dom (f,a) by A3, XBOOLE_0:def_4; then a <= f . x by Def14; then not x in less_dom (f,a) by Def11; then not x in A /\ (less_dom (f,a)) by XBOOLE_0:def_4; hence x in A \ (A /\ (less_dom (f,a))) by A4, XBOOLE_0:def_5; ::_thesis: verum end; then A5: A /\ (great_eq_dom (f,a)) c= A \ (A /\ (less_dom (f,a))) by TARSKI:def_3; for x being set st x in A \ (A /\ (less_dom (f,a))) holds x in A /\ (great_eq_dom (f,a)) proof let x be set ; ::_thesis: ( x in A \ (A /\ (less_dom (f,a))) implies x in A /\ (great_eq_dom (f,a)) ) assume A6: x in A \ (A /\ (less_dom (f,a))) ; ::_thesis: x in A /\ (great_eq_dom (f,a)) then A7: x in A ; not x in A /\ (less_dom (f,a)) by A6, XBOOLE_0:def_5; then A8: not x in less_dom (f,a) by A6, XBOOLE_0:def_4; reconsider x = x as Element of X by A2, A7; reconsider y = f . x as R_eal ; not y < a by A1, A7, A8, Def11; then x in great_eq_dom (f,a) by A1, A7, Def14; hence x in A /\ (great_eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A \ (A /\ (less_dom (f,a))) c= A /\ (great_eq_dom (f,a)) by TARSKI:def_3; hence A /\ (great_eq_dom (f,a)) = A \ (A /\ (less_dom (f,a))) by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th15: :: MESFUNC1:15 for X being set for f being PartFunc of X,ExtREAL for A being set for a being R_eal st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) proof let X be set ; ::_thesis: for f being PartFunc of X,ExtREAL for A being set for a being R_eal st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set for a being R_eal st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) let A be set ; ::_thesis: for a being R_eal st A c= dom f holds A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) let a be R_eal; ::_thesis: ( A c= dom f implies A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) ) assume A1: A c= dom f ; ::_thesis: A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) dom f c= X by RELAT_1:def_18; then A2: A c= X by A1, XBOOLE_1:1; for x being set st x in A /\ (great_dom (f,a)) holds x in A \ (A /\ (less_eq_dom (f,a))) proof let x be set ; ::_thesis: ( x in A /\ (great_dom (f,a)) implies x in A \ (A /\ (less_eq_dom (f,a))) ) assume A3: x in A /\ (great_dom (f,a)) ; ::_thesis: x in A \ (A /\ (less_eq_dom (f,a))) then A4: x in A by XBOOLE_0:def_4; x in great_dom (f,a) by A3, XBOOLE_0:def_4; then a < f . x by Def13; then not x in less_eq_dom (f,a) by Def12; then not x in A /\ (less_eq_dom (f,a)) by XBOOLE_0:def_4; hence x in A \ (A /\ (less_eq_dom (f,a))) by A4, XBOOLE_0:def_5; ::_thesis: verum end; then A5: A /\ (great_dom (f,a)) c= A \ (A /\ (less_eq_dom (f,a))) by TARSKI:def_3; for x being set st x in A \ (A /\ (less_eq_dom (f,a))) holds x in A /\ (great_dom (f,a)) proof let x be set ; ::_thesis: ( x in A \ (A /\ (less_eq_dom (f,a))) implies x in A /\ (great_dom (f,a)) ) assume A6: x in A \ (A /\ (less_eq_dom (f,a))) ; ::_thesis: x in A /\ (great_dom (f,a)) then A7: x in A ; not x in A /\ (less_eq_dom (f,a)) by A6, XBOOLE_0:def_5; then A8: not x in less_eq_dom (f,a) by A6, XBOOLE_0:def_4; reconsider x = x as Element of X by A2, A7; reconsider y = f . x as R_eal ; not y <= a by A1, A7, A8, Def12; then x in great_dom (f,a) by A1, A7, Def13; hence x in A /\ (great_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A \ (A /\ (less_eq_dom (f,a))) c= A /\ (great_dom (f,a)) by TARSKI:def_3; hence A /\ (great_dom (f,a)) = A \ (A /\ (less_eq_dom (f,a))) by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th16: :: MESFUNC1:16 for X being set for f being PartFunc of X,ExtREAL for A being set for a being R_eal st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) proof let X be set ; ::_thesis: for f being PartFunc of X,ExtREAL for A being set for a being R_eal st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set for a being R_eal st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) let A be set ; ::_thesis: for a being R_eal st A c= dom f holds A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) let a be R_eal; ::_thesis: ( A c= dom f implies A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) ) assume A1: A c= dom f ; ::_thesis: A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) dom f c= X by RELAT_1:def_18; then A2: A c= X by A1, XBOOLE_1:1; A3: A /\ (less_eq_dom (f,a)) c= A \ (A /\ (great_dom (f,a))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A /\ (less_eq_dom (f,a)) or x in A \ (A /\ (great_dom (f,a))) ) assume A4: x in A /\ (less_eq_dom (f,a)) ; ::_thesis: x in A \ (A /\ (great_dom (f,a))) then A5: x in A by XBOOLE_0:def_4; x in less_eq_dom (f,a) by A4, XBOOLE_0:def_4; then f . x <= a by Def12; then not x in great_dom (f,a) by Def13; then not x in A /\ (great_dom (f,a)) by XBOOLE_0:def_4; hence x in A \ (A /\ (great_dom (f,a))) by A5, XBOOLE_0:def_5; ::_thesis: verum end; for x being set st x in A \ (A /\ (great_dom (f,a))) holds x in A /\ (less_eq_dom (f,a)) proof let x be set ; ::_thesis: ( x in A \ (A /\ (great_dom (f,a))) implies x in A /\ (less_eq_dom (f,a)) ) assume A6: x in A \ (A /\ (great_dom (f,a))) ; ::_thesis: x in A /\ (less_eq_dom (f,a)) then A7: x in A ; not x in A /\ (great_dom (f,a)) by A6, XBOOLE_0:def_5; then A8: not x in great_dom (f,a) by A6, XBOOLE_0:def_4; reconsider x = x as Element of X by A2, A7; reconsider y = f . x as R_eal ; not a < y by A1, A7, A8, Def13; then x in less_eq_dom (f,a) by A1, A7, Def12; hence x in A /\ (less_eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A \ (A /\ (great_dom (f,a))) c= A /\ (less_eq_dom (f,a)) by TARSKI:def_3; hence A /\ (less_eq_dom (f,a)) = A \ (A /\ (great_dom (f,a))) by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th17: :: MESFUNC1:17 for X being set for f being PartFunc of X,ExtREAL for A being set for a being R_eal st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) proof let X be set ; ::_thesis: for f being PartFunc of X,ExtREAL for A being set for a being R_eal st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set for a being R_eal st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) let A be set ; ::_thesis: for a being R_eal st A c= dom f holds A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) let a be R_eal; ::_thesis: ( A c= dom f implies A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) ) assume A1: A c= dom f ; ::_thesis: A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) dom f c= X by RELAT_1:def_18; then A2: A c= X by A1, XBOOLE_1:1; for x being set st x in A /\ (less_dom (f,a)) holds x in A \ (A /\ (great_eq_dom (f,a))) proof let x be set ; ::_thesis: ( x in A /\ (less_dom (f,a)) implies x in A \ (A /\ (great_eq_dom (f,a))) ) assume A3: x in A /\ (less_dom (f,a)) ; ::_thesis: x in A \ (A /\ (great_eq_dom (f,a))) then A4: x in A by XBOOLE_0:def_4; x in less_dom (f,a) by A3, XBOOLE_0:def_4; then f . x < a by Def11; then not x in great_eq_dom (f,a) by Def14; then not x in A /\ (great_eq_dom (f,a)) by XBOOLE_0:def_4; hence x in A \ (A /\ (great_eq_dom (f,a))) by A4, XBOOLE_0:def_5; ::_thesis: verum end; then A5: A /\ (less_dom (f,a)) c= A \ (A /\ (great_eq_dom (f,a))) by TARSKI:def_3; for x being set st x in A \ (A /\ (great_eq_dom (f,a))) holds x in A /\ (less_dom (f,a)) proof let x be set ; ::_thesis: ( x in A \ (A /\ (great_eq_dom (f,a))) implies x in A /\ (less_dom (f,a)) ) assume A6: x in A \ (A /\ (great_eq_dom (f,a))) ; ::_thesis: x in A /\ (less_dom (f,a)) then A7: x in A ; not x in A /\ (great_eq_dom (f,a)) by A6, XBOOLE_0:def_5; then A8: not x in great_eq_dom (f,a) by A6, XBOOLE_0:def_4; reconsider x = x as Element of X by A2, A7; reconsider y = f . x as R_eal ; not a <= y by A1, A7, A8, Def14; then x in less_dom (f,a) by A1, A7, Def11; hence x in A /\ (less_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A \ (A /\ (great_eq_dom (f,a))) c= A /\ (less_dom (f,a)) by TARSKI:def_3; hence A /\ (less_dom (f,a)) = A \ (A /\ (great_eq_dom (f,a))) by A5, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MESFUNC1:18 for X being set for f being PartFunc of X,ExtREAL for A being set for a being R_eal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) proof let X be set ; ::_thesis: for f being PartFunc of X,ExtREAL for A being set for a being R_eal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set for a being R_eal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) let A be set ; ::_thesis: for a being R_eal holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) let a be R_eal; ::_thesis: A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) for x being set st x in A /\ (eq_dom (f,a)) holds x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) proof let x be set ; ::_thesis: ( x in A /\ (eq_dom (f,a)) implies x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) ) assume A1: x in A /\ (eq_dom (f,a)) ; ::_thesis: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) then A2: x in A by XBOOLE_0:def_4; A3: x in eq_dom (f,a) by A1, XBOOLE_0:def_4; then A4: a = f . x by Def15; reconsider x = x as Element of X by A1; A5: x in dom f by A3, Def15; then x in great_eq_dom (f,a) by A4, Def14; then A6: x in A /\ (great_eq_dom (f,a)) by A2, XBOOLE_0:def_4; x in less_eq_dom (f,a) by A4, A5, Def12; hence x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A6, XBOOLE_0:def_4; ::_thesis: verum end; then A7: A /\ (eq_dom (f,a)) c= (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by TARSKI:def_3; for x being set st x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) holds x in A /\ (eq_dom (f,a)) proof let x be set ; ::_thesis: ( x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) implies x in A /\ (eq_dom (f,a)) ) assume A8: x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) ; ::_thesis: x in A /\ (eq_dom (f,a)) then A9: x in A /\ (great_eq_dom (f,a)) by XBOOLE_0:def_4; A10: x in less_eq_dom (f,a) by A8, XBOOLE_0:def_4; A11: x in A by A9, XBOOLE_0:def_4; x in great_eq_dom (f,a) by A9, XBOOLE_0:def_4; then A12: a <= f . x by Def14; A13: f . x <= a by A10, Def12; reconsider x = x as Element of X by A8; A14: x in dom f by A10, Def12; a = f . x by A12, A13, XXREAL_0:1; then x in eq_dom (f,a) by A14, Def15; hence x in A /\ (eq_dom (f,a)) by A11, XBOOLE_0:def_4; ::_thesis: verum end; then (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) c= A /\ (eq_dom (f,a)) by TARSKI:def_3; hence A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) by A7, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: MESFUNC1:19 for X being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) proof let X be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,ExtREAL for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) let A be set ; ::_thesis: for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) let r be Real; ::_thesis: ( ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) implies A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) ) assume A1: for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (r - (1 / (n + 1)))))) ; ::_thesis: A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) for x being set st x in A /\ (great_eq_dom (f,(R_EAL r))) holds x in meet (rng F) proof let x be set ; ::_thesis: ( x in A /\ (great_eq_dom (f,(R_EAL r))) implies x in meet (rng F) ) assume A2: x in A /\ (great_eq_dom (f,(R_EAL r))) ; ::_thesis: x in meet (rng F) then A3: x in A by XBOOLE_0:def_4; A4: x in great_eq_dom (f,(R_EAL r)) by A2, XBOOLE_0:def_4; for Y being set st Y in rng F holds x in Y proof let Y be set ; ::_thesis: ( Y in rng F implies x in Y ) ( Y in rng F implies x in Y ) proof assume Y in rng F ; ::_thesis: x in Y then consider m being Element of NAT such that m in dom F and A5: Y = F . m by PARTFUN1:3; A6: Y = A /\ (great_dom (f,(R_EAL (r - (1 / (m + 1)))))) by A1, A5; A7: x in dom f by A4, Def14; reconsider x = x as Element of X by A2; A8: R_EAL r <= f . x by A4, Def14; (m + 1) " > 0 ; then 1 / (m + 1) > 0 by XCMPLX_1:215; then r < r + (1 / (m + 1)) by XREAL_1:29; then R_EAL (r - (1 / (m + 1))) < R_EAL r by XREAL_1:19; then R_EAL (r - (1 / (m + 1))) < f . x by A8, XXREAL_0:2; then x in great_dom (f,(R_EAL (r - (1 / (m + 1))))) by A7, Def13; hence x in Y by A3, A6, XBOOLE_0:def_4; ::_thesis: verum end; hence ( Y in rng F implies x in Y ) ; ::_thesis: verum end; hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum end; then A9: A /\ (great_eq_dom (f,(R_EAL r))) c= meet (rng F) by TARSKI:def_3; for x being set st x in meet (rng F) holds x in A /\ (great_eq_dom (f,(R_EAL r))) proof let x be set ; ::_thesis: ( x in meet (rng F) implies x in A /\ (great_eq_dom (f,(R_EAL r))) ) assume A10: x in meet (rng F) ; ::_thesis: x in A /\ (great_eq_dom (f,(R_EAL r))) A11: for m being Element of NAT holds ( x in A & x in dom f & R_EAL (r - (1 / (m + 1))) < f . x ) proof let m be Element of NAT ; ::_thesis: ( x in A & x in dom f & R_EAL (r - (1 / (m + 1))) < f . x ) m in NAT ; then m in dom F by FUNCT_2:def_1; then F . m in rng F by FUNCT_1:def_3; then x in F . m by A10, SETFAM_1:def_1; then A12: x in A /\ (great_dom (f,(R_EAL (r - (1 / (m + 1)))))) by A1; then x in great_dom (f,(R_EAL (r - (1 / (m + 1))))) by XBOOLE_0:def_4; hence ( x in A & x in dom f & R_EAL (r - (1 / (m + 1))) < f . x ) by A12, Def13, XBOOLE_0:def_4; ::_thesis: verum end; reconsider y = f . x as R_eal ; 1 in NAT ; then 1 in dom F by FUNCT_2:def_1; then F . 1 in rng F by FUNCT_1:def_3; then x in F . 1 by A10, SETFAM_1:def_1; then x in A /\ (great_dom (f,(R_EAL (r - (1 / (1 + 1)))))) by A1; then reconsider x = x as Element of X ; R_EAL r <= y proof now__::_thesis:_R_EAL_r_<=_y percases ( y = +infty or not y = +infty ) ; suppose y = +infty ; ::_thesis: R_EAL r <= y hence R_EAL r <= y by XXREAL_0:4; ::_thesis: verum end; suppose not y = +infty ; ::_thesis: R_EAL r <= y then A13: not +infty <= y by XXREAL_0:4; R_EAL (r - (1 / (1 + 1))) < y by A11; then reconsider y1 = y as Real by A13, XXREAL_0:48; for m being Element of NAT holds r - (1 / (m + 1)) <= y1 proof let m be Element of NAT ; ::_thesis: r - (1 / (m + 1)) <= y1 R_EAL (r - (1 / (m + 1))) < R_EAL y1 by A11; hence r - (1 / (m + 1)) <= y1 ; ::_thesis: verum end; hence R_EAL r <= y by Th11; ::_thesis: verum end; end; end; hence R_EAL r <= y ; ::_thesis: verum end; then x in great_eq_dom (f,(R_EAL r)) by A11, Def14; hence x in A /\ (great_eq_dom (f,(R_EAL r))) by A11, XBOOLE_0:def_4; ::_thesis: verum end; then meet (rng F) c= A /\ (great_eq_dom (f,(R_EAL r))) by TARSKI:def_3; hence A /\ (great_eq_dom (f,(R_EAL r))) = meet (rng F) by A9, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th20: :: MESFUNC1:20 for X being set for f being PartFunc of X,ExtREAL for S being SigmaField of X for F being Function of NAT,S for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) proof let X be set ; ::_thesis: for f being PartFunc of X,ExtREAL for S being SigmaField of X for F being Function of NAT,S for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) let f be PartFunc of X,ExtREAL; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) let F be Function of NAT,S; ::_thesis: for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) let A be set ; ::_thesis: for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) let r be real number ; ::_thesis: ( ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) implies A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) ) assume A1: for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) ; ::_thesis: A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) for x being set st x in A /\ (less_eq_dom (f,(R_EAL r))) holds x in meet (rng F) proof let x be set ; ::_thesis: ( x in A /\ (less_eq_dom (f,(R_EAL r))) implies x in meet (rng F) ) assume A2: x in A /\ (less_eq_dom (f,(R_EAL r))) ; ::_thesis: x in meet (rng F) then A3: x in A by XBOOLE_0:def_4; A4: x in less_eq_dom (f,(R_EAL r)) by A2, XBOOLE_0:def_4; for Y being set st Y in rng F holds x in Y proof let Y be set ; ::_thesis: ( Y in rng F implies x in Y ) ( Y in rng F implies x in Y ) proof assume Y in rng F ; ::_thesis: x in Y then consider m being Element of NAT such that m in dom F and A5: Y = F . m by PARTFUN1:3; A6: Y = A /\ (less_dom (f,(R_EAL (r + (1 / (m + 1)))))) by A1, A5; A7: x in dom f by A4, Def12; reconsider x = x as Element of X by A2; A8: f . x <= R_EAL r by A4, Def12; (m + 1) " > 0 ; then 1 / (m + 1) > 0 by XCMPLX_1:215; then R_EAL r < R_EAL (r + (1 / (m + 1))) by XREAL_1:29; then f . x < R_EAL (r + (1 / (m + 1))) by A8, XXREAL_0:2; then x in less_dom (f,(R_EAL (r + (1 / (m + 1))))) by A7, Def11; hence x in Y by A3, A6, XBOOLE_0:def_4; ::_thesis: verum end; hence ( Y in rng F implies x in Y ) ; ::_thesis: verum end; hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum end; then A9: A /\ (less_eq_dom (f,(R_EAL r))) c= meet (rng F) by TARSKI:def_3; for x being set st x in meet (rng F) holds x in A /\ (less_eq_dom (f,(R_EAL r))) proof let x be set ; ::_thesis: ( x in meet (rng F) implies x in A /\ (less_eq_dom (f,(R_EAL r))) ) assume A10: x in meet (rng F) ; ::_thesis: x in A /\ (less_eq_dom (f,(R_EAL r))) A11: for m being Element of NAT holds ( x in A & x in dom f & f . x < R_EAL (r + (1 / (m + 1))) ) proof let m be Element of NAT ; ::_thesis: ( x in A & x in dom f & f . x < R_EAL (r + (1 / (m + 1))) ) m in NAT ; then m in dom F by FUNCT_2:def_1; then F . m in rng F by FUNCT_1:def_3; then x in F . m by A10, SETFAM_1:def_1; then A12: x in A /\ (less_dom (f,(R_EAL (r + (1 / (m + 1)))))) by A1; then x in less_dom (f,(R_EAL (r + (1 / (m + 1))))) by XBOOLE_0:def_4; hence ( x in A & x in dom f & f . x < R_EAL (r + (1 / (m + 1))) ) by A12, Def11, XBOOLE_0:def_4; ::_thesis: verum end; reconsider y = f . x as R_eal ; 1 in NAT ; then 1 in dom F by FUNCT_2:def_1; then F . 1 in rng F by FUNCT_1:def_3; then x in F . 1 by A10, SETFAM_1:def_1; then x in A /\ (less_dom (f,(R_EAL (r + (1 / (1 + 1)))))) by A1; then reconsider x = x as Element of X ; y <= R_EAL r proof now__::_thesis:_y_<=_R_EAL_r percases ( y = -infty or not y = -infty ) ; suppose y = -infty ; ::_thesis: y <= R_EAL r hence y <= R_EAL r by XXREAL_0:5; ::_thesis: verum end; suppose not y = -infty ; ::_thesis: y <= R_EAL r then A13: not y <= -infty by XXREAL_0:6; y < R_EAL (r + (1 / (1 + 1))) by A11; then reconsider y1 = y as Real by A13, XXREAL_0:48; for m being Element of NAT holds y1 - (1 / (m + 1)) <= r proof let m be Element of NAT ; ::_thesis: y1 - (1 / (m + 1)) <= r R_EAL y1 < R_EAL (r + (1 / (m + 1))) by A11; hence y1 - (1 / (m + 1)) <= r by XREAL_1:20; ::_thesis: verum end; hence y <= R_EAL r by Th11; ::_thesis: verum end; end; end; hence y <= R_EAL r ; ::_thesis: verum end; then x in less_eq_dom (f,(R_EAL r)) by A11, Def12; hence x in A /\ (less_eq_dom (f,(R_EAL r))) by A11, XBOOLE_0:def_4; ::_thesis: verum end; then meet (rng F) c= A /\ (less_eq_dom (f,(R_EAL r))) by TARSKI:def_3; hence A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) by A9, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th21: :: MESFUNC1:21 for X being set for f being PartFunc of X,ExtREAL for S being SigmaField of X for F being Function of NAT,S for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (less_dom (f,(R_EAL r))) = union (rng F) proof let X be set ; ::_thesis: for f being PartFunc of X,ExtREAL for S being SigmaField of X for F being Function of NAT,S for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (less_dom (f,(R_EAL r))) = union (rng F) let f be PartFunc of X,ExtREAL; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (less_dom (f,(R_EAL r))) = union (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (less_dom (f,(R_EAL r))) = union (rng F) let F be Function of NAT,S; ::_thesis: for A being set for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (less_dom (f,(R_EAL r))) = union (rng F) let A be set ; ::_thesis: for r being real number st ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) holds A /\ (less_dom (f,(R_EAL r))) = union (rng F) let r be real number ; ::_thesis: ( ( for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ) implies A /\ (less_dom (f,(R_EAL r))) = union (rng F) ) assume A1: for n being Element of NAT holds F . n = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) ; ::_thesis: A /\ (less_dom (f,(R_EAL r))) = union (rng F) for x being set st x in A /\ (less_dom (f,(R_EAL r))) holds x in union (rng F) proof let x be set ; ::_thesis: ( x in A /\ (less_dom (f,(R_EAL r))) implies x in union (rng F) ) assume A2: x in A /\ (less_dom (f,(R_EAL r))) ; ::_thesis: x in union (rng F) then A3: x in A by XBOOLE_0:def_4; A4: x in less_dom (f,(R_EAL r)) by A2, XBOOLE_0:def_4; ex Y being set st ( x in Y & Y in rng F ) proof reconsider x = x as Element of X by A2; A5: x in dom f by A4, Def11; A6: f . x < R_EAL r by A4, Def11; ex m being Element of NAT st f . x <= R_EAL (r - (1 / (m + 1))) proof percases ( f . x = -infty or not f . x = -infty ) ; supposeA7: f . x = -infty ; ::_thesis: ex m being Element of NAT st f . x <= R_EAL (r - (1 / (m + 1))) take 1 ; ::_thesis: f . x <= R_EAL (r - (1 / (1 + 1))) thus f . x <= R_EAL (r - (1 / (1 + 1))) by A7, XXREAL_0:5; ::_thesis: verum end; suppose not f . x = -infty ; ::_thesis: ex m being Element of NAT st f . x <= R_EAL (r - (1 / (m + 1))) then not f . x <= -infty by XXREAL_0:6; then reconsider y1 = f . x as Real by A6, XXREAL_0:48; consider m being Element of NAT such that A8: 1 / (m + 1) < r - y1 by A6, Th10; y1 + (1 / (m + 1)) < r by A8, XREAL_1:20; then f . x <= R_EAL (r - (1 / (m + 1))) by XREAL_1:20; hence ex m being Element of NAT st f . x <= R_EAL (r - (1 / (m + 1))) ; ::_thesis: verum end; end; end; then consider m being Element of NAT such that A9: f . x <= R_EAL (r - (1 / (m + 1))) ; x in less_eq_dom (f,(R_EAL (r - (1 / (m + 1))))) by A5, A9, Def12; then A10: x in A /\ (less_eq_dom (f,(R_EAL (r - (1 / (m + 1)))))) by A3, XBOOLE_0:def_4; m in NAT ; then A11: m in dom F by FUNCT_2:def_1; take F . m ; ::_thesis: ( x in F . m & F . m in rng F ) thus ( x in F . m & F . m in rng F ) by A1, A10, A11, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum end; then A12: A /\ (less_dom (f,(R_EAL r))) c= union (rng F) by TARSKI:def_3; for x being set st x in union (rng F) holds x in A /\ (less_dom (f,(R_EAL r))) proof let x be set ; ::_thesis: ( x in union (rng F) implies x in A /\ (less_dom (f,(R_EAL r))) ) assume x in union (rng F) ; ::_thesis: x in A /\ (less_dom (f,(R_EAL r))) then consider Y being set such that A13: x in Y and A14: Y in rng F by TARSKI:def_4; consider m being Element of NAT such that m in dom F and A15: F . m = Y by A14, PARTFUN1:3; A16: x in A /\ (less_eq_dom (f,(R_EAL (r - (1 / (m + 1)))))) by A1, A13, A15; then A17: x in A by XBOOLE_0:def_4; A18: x in less_eq_dom (f,(R_EAL (r - (1 / (m + 1))))) by A16, XBOOLE_0:def_4; then A19: x in dom f by Def12; A20: f . x <= R_EAL (r - (1 / (m + 1))) by A18, Def12; reconsider x = x as Element of X by A13, A14; f . x < R_EAL r proof now__::_thesis:_f_._x_<_R_EAL_r r < r + (1 / (m + 1)) by XREAL_1:29, XREAL_1:139; then r - (1 / (m + 1)) < r by XREAL_1:19; hence f . x < R_EAL r by A20, XXREAL_0:2; ::_thesis: verum end; hence f . x < R_EAL r ; ::_thesis: verum end; then x in less_dom (f,(R_EAL r)) by A19, Def11; hence x in A /\ (less_dom (f,(R_EAL r))) by A17, XBOOLE_0:def_4; ::_thesis: verum end; then union (rng F) c= A /\ (less_dom (f,(R_EAL r))) by TARSKI:def_3; hence A /\ (less_dom (f,(R_EAL r))) = union (rng F) by A12, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th22: :: MESFUNC1:22 for X being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (great_dom (f,(R_EAL r))) = union (rng F) proof let X be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (great_dom (f,(R_EAL r))) = union (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (great_dom (f,(R_EAL r))) = union (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,ExtREAL for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (great_dom (f,(R_EAL r))) = union (rng F) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (great_dom (f,(R_EAL r))) = union (rng F) let A be set ; ::_thesis: for r being Real st ( for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) holds A /\ (great_dom (f,(R_EAL r))) = union (rng F) let r be Real; ::_thesis: ( ( for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ) implies A /\ (great_dom (f,(R_EAL r))) = union (rng F) ) assume A1: for n being Element of NAT holds F . n = A /\ (great_eq_dom (f,(R_EAL (r + (1 / (n + 1)))))) ; ::_thesis: A /\ (great_dom (f,(R_EAL r))) = union (rng F) for x being set st x in A /\ (great_dom (f,(R_EAL r))) holds x in union (rng F) proof let x be set ; ::_thesis: ( x in A /\ (great_dom (f,(R_EAL r))) implies x in union (rng F) ) assume A2: x in A /\ (great_dom (f,(R_EAL r))) ; ::_thesis: x in union (rng F) then A3: x in A by XBOOLE_0:def_4; A4: x in great_dom (f,(R_EAL r)) by A2, XBOOLE_0:def_4; ex Y being set st ( x in Y & Y in rng F ) proof reconsider x = x as Element of X by A2; A5: x in dom f by A4, Def13; A6: R_EAL r < f . x by A4, Def13; ex m being Element of NAT st R_EAL (r + (1 / (m + 1))) <= f . x proof percases ( f . x = +infty or not f . x = +infty ) ; supposeA7: f . x = +infty ; ::_thesis: ex m being Element of NAT st R_EAL (r + (1 / (m + 1))) <= f . x take 1 ; ::_thesis: R_EAL (r + (1 / (1 + 1))) <= f . x thus R_EAL (r + (1 / (1 + 1))) <= f . x by A7, XXREAL_0:4; ::_thesis: verum end; suppose not f . x = +infty ; ::_thesis: ex m being Element of NAT st R_EAL (r + (1 / (m + 1))) <= f . x then not +infty <= f . x by XXREAL_0:4; then reconsider y1 = f . x as Real by A6, XXREAL_0:48; consider m being Element of NAT such that A8: 1 / (m + 1) < y1 - r by A6, Th10; take m ; ::_thesis: R_EAL (r + (1 / (m + 1))) <= f . x thus R_EAL (r + (1 / (m + 1))) <= f . x by A8, XREAL_1:20; ::_thesis: verum end; end; end; then consider m being Element of NAT such that A9: R_EAL (r + (1 / (m + 1))) <= f . x ; x in great_eq_dom (f,(R_EAL (r + (1 / (m + 1))))) by A5, A9, Def14; then A10: x in A /\ (great_eq_dom (f,(R_EAL (r + (1 / (m + 1)))))) by A3, XBOOLE_0:def_4; m in NAT ; then A11: m in dom F by FUNCT_2:def_1; take F . m ; ::_thesis: ( x in F . m & F . m in rng F ) thus ( x in F . m & F . m in rng F ) by A1, A10, A11, FUNCT_1:def_3; ::_thesis: verum end; hence x in union (rng F) by TARSKI:def_4; ::_thesis: verum end; then A12: A /\ (great_dom (f,(R_EAL r))) c= union (rng F) by TARSKI:def_3; for x being set st x in union (rng F) holds x in A /\ (great_dom (f,(R_EAL r))) proof let x be set ; ::_thesis: ( x in union (rng F) implies x in A /\ (great_dom (f,(R_EAL r))) ) assume x in union (rng F) ; ::_thesis: x in A /\ (great_dom (f,(R_EAL r))) then consider Y being set such that A13: x in Y and A14: Y in rng F by TARSKI:def_4; consider m being Element of NAT such that m in dom F and A15: F . m = Y by A14, PARTFUN1:3; A16: x in A /\ (great_eq_dom (f,(R_EAL (r + (1 / (m + 1)))))) by A1, A13, A15; then A17: x in A by XBOOLE_0:def_4; A18: x in great_eq_dom (f,(R_EAL (r + (1 / (m + 1))))) by A16, XBOOLE_0:def_4; then A19: x in dom f by Def14; A20: R_EAL (r + (1 / (m + 1))) <= f . x by A18, Def14; reconsider x = x as Element of X by A13, A14; R_EAL r < f . x proof now__::_thesis:_R_EAL_r_<_f_._x r < r + (1 / (m + 1)) by XREAL_1:29, XREAL_1:139; hence R_EAL r < f . x by A20, XXREAL_0:2; ::_thesis: verum end; hence R_EAL r < f . x ; ::_thesis: verum end; then x in great_dom (f,(R_EAL r)) by A19, Def13; hence x in A /\ (great_dom (f,(R_EAL r))) by A17, XBOOLE_0:def_4; ::_thesis: verum end; then union (rng F) c= A /\ (great_dom (f,(R_EAL r))) by TARSKI:def_3; hence A /\ (great_dom (f,(R_EAL r))) = union (rng F) by A12, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th23: :: MESFUNC1:23 for X being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL n))) ) holds A /\ (eq_dom (f,+infty)) = meet (rng F) proof let X be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL n))) ) holds A /\ (eq_dom (f,+infty)) = meet (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL n))) ) holds A /\ (eq_dom (f,+infty)) = meet (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL n))) ) holds A /\ (eq_dom (f,+infty)) = meet (rng F) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL n))) ) holds A /\ (eq_dom (f,+infty)) = meet (rng F) let A be set ; ::_thesis: ( ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL n))) ) implies A /\ (eq_dom (f,+infty)) = meet (rng F) ) assume A1: for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL n))) ; ::_thesis: A /\ (eq_dom (f,+infty)) = meet (rng F) for x being set st x in A /\ (eq_dom (f,+infty)) holds x in meet (rng F) proof let x be set ; ::_thesis: ( x in A /\ (eq_dom (f,+infty)) implies x in meet (rng F) ) assume A2: x in A /\ (eq_dom (f,+infty)) ; ::_thesis: x in meet (rng F) then A3: x in A by XBOOLE_0:def_4; A4: x in eq_dom (f,+infty) by A2, XBOOLE_0:def_4; for Y being set st Y in rng F holds x in Y proof let Y be set ; ::_thesis: ( Y in rng F implies x in Y ) ( Y in rng F implies x in Y ) proof assume Y in rng F ; ::_thesis: x in Y then consider m being Element of NAT such that m in dom F and A5: Y = F . m by PARTFUN1:3; A6: Y = A /\ (great_dom (f,(R_EAL m))) by A1, A5; reconsider x = x as Element of X by A2; A7: f . x = +infty by A4, Def15; ( x in dom f & not +infty <= R_EAL m ) by A4, Def15, XXREAL_0:9; then x in great_dom (f,(R_EAL m)) by A7, Def13; hence x in Y by A3, A6, XBOOLE_0:def_4; ::_thesis: verum end; hence ( Y in rng F implies x in Y ) ; ::_thesis: verum end; hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum end; then A8: A /\ (eq_dom (f,+infty)) c= meet (rng F) by TARSKI:def_3; for x being set st x in meet (rng F) holds x in A /\ (eq_dom (f,+infty)) proof let x be set ; ::_thesis: ( x in meet (rng F) implies x in A /\ (eq_dom (f,+infty)) ) assume A9: x in meet (rng F) ; ::_thesis: x in A /\ (eq_dom (f,+infty)) A10: for m being Element of NAT holds ( x in A & x in dom f & ex y being R_eal st ( y = f . x & y = +infty ) ) proof let m be Element of NAT ; ::_thesis: ( x in A & x in dom f & ex y being R_eal st ( y = f . x & y = +infty ) ) m in NAT ; then m in dom F by FUNCT_2:def_1; then F . m in rng F by FUNCT_1:def_3; then x in F . m by A9, SETFAM_1:def_1; then A11: x in A /\ (great_dom (f,(R_EAL m))) by A1; then A12: x in great_dom (f,(R_EAL m)) by XBOOLE_0:def_4; for r being Real holds R_EAL r < f . x proof let r be Real; ::_thesis: R_EAL r < f . x consider n being Element of NAT such that A13: r <= n by Th8; n in NAT ; then n in dom F by FUNCT_2:def_1; then F . n in rng F by FUNCT_1:def_3; then x in F . n by A9, SETFAM_1:def_1; then x in A /\ (great_dom (f,(R_EAL n))) by A1; then x in great_dom (f,(R_EAL n)) by XBOOLE_0:def_4; then R_EAL n < f . x by Def13; hence R_EAL r < f . x by A13, XXREAL_0:2; ::_thesis: verum end; then f . x = +infty by Th12; hence ( x in A & x in dom f & ex y being R_eal st ( y = f . x & y = +infty ) ) by A11, A12, Def13, XBOOLE_0:def_4; ::_thesis: verum end; 1 in NAT ; then 1 in dom F by FUNCT_2:def_1; then F . 1 in rng F by FUNCT_1:def_3; then x in F . 1 by A9, SETFAM_1:def_1; then x in A /\ (great_dom (f,(R_EAL 1))) by A1; then reconsider x = x as Element of X ; x in eq_dom (f,+infty) by A10, Def15; hence x in A /\ (eq_dom (f,+infty)) by A10, XBOOLE_0:def_4; ::_thesis: verum end; then meet (rng F) c= A /\ (eq_dom (f,+infty)) by TARSKI:def_3; hence A /\ (eq_dom (f,+infty)) = meet (rng F) by A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th24: :: MESFUNC1:24 for X being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL n))) ) holds A /\ (less_dom (f,+infty)) = union (rng F) proof let X be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL n))) ) holds A /\ (less_dom (f,+infty)) = union (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL n))) ) holds A /\ (less_dom (f,+infty)) = union (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL n))) ) holds A /\ (less_dom (f,+infty)) = union (rng F) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL n))) ) holds A /\ (less_dom (f,+infty)) = union (rng F) let A be set ; ::_thesis: ( ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL n))) ) implies A /\ (less_dom (f,+infty)) = union (rng F) ) assume A1: for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL n))) ; ::_thesis: A /\ (less_dom (f,+infty)) = union (rng F) for x being set st x in A /\ (less_dom (f,+infty)) holds x in union (rng F) proof let x be set ; ::_thesis: ( x in A /\ (less_dom (f,+infty)) implies x in union (rng F) ) assume A2: x in A /\ (less_dom (f,+infty)) ; ::_thesis: x in union (rng F) then A3: x in A by XBOOLE_0:def_4; A4: x in less_dom (f,+infty) by A2, XBOOLE_0:def_4; then A5: x in dom f by Def11; A6: f . x < +infty by A4, Def11; ex n being Element of NAT st f . x < R_EAL n proof percases ( f . x = -infty or not f . x = -infty ) ; supposeA7: f . x = -infty ; ::_thesis: ex n being Element of NAT st f . x < R_EAL n take 0 ; ::_thesis: f . x < R_EAL 0 thus f . x < R_EAL 0 by A7; ::_thesis: verum end; suppose not f . x = -infty ; ::_thesis: ex n being Element of NAT st f . x < R_EAL n then not f . x <= -infty by XXREAL_0:6; then reconsider y1 = f . x as Real by A6, XXREAL_0:48; consider n1 being Element of NAT such that A8: y1 <= n1 by Th8; A9: n1 < n1 + 1 by NAT_1:13; reconsider m = n1 + 1 as Element of NAT ; take m ; ::_thesis: f . x < R_EAL m thus f . x < R_EAL m by A8, A9, XXREAL_0:2; ::_thesis: verum end; end; end; then consider n being Element of NAT such that A10: f . x < R_EAL n ; reconsider x = x as Element of X by A2; x in less_dom (f,(R_EAL n)) by A5, A10, Def11; then x in A /\ (less_dom (f,(R_EAL n))) by A3, XBOOLE_0:def_4; then A11: x in F . n by A1; n in NAT ; then n in dom F by FUNCT_2:def_1; then F . n in rng F by FUNCT_1:def_3; hence x in union (rng F) by A11, TARSKI:def_4; ::_thesis: verum end; then A12: A /\ (less_dom (f,+infty)) c= union (rng F) by TARSKI:def_3; for x being set st x in union (rng F) holds x in A /\ (less_dom (f,+infty)) proof let x be set ; ::_thesis: ( x in union (rng F) implies x in A /\ (less_dom (f,+infty)) ) assume x in union (rng F) ; ::_thesis: x in A /\ (less_dom (f,+infty)) then consider Y being set such that A13: x in Y and A14: Y in rng F by TARSKI:def_4; consider m being Element of NAT such that m in dom F and A15: F . m = Y by A14, PARTFUN1:3; A16: x in A /\ (less_dom (f,(R_EAL m))) by A1, A13, A15; then A17: x in A by XBOOLE_0:def_4; A18: x in less_dom (f,(R_EAL m)) by A16, XBOOLE_0:def_4; then A19: x in dom f by Def11; A20: f . x < R_EAL m by A18, Def11; reconsider x = x as Element of X by A13, A14; f . x < +infty by A20, XXREAL_0:2, XXREAL_0:9; then x in less_dom (f,+infty) by A19, Def11; hence x in A /\ (less_dom (f,+infty)) by A17, XBOOLE_0:def_4; ::_thesis: verum end; then union (rng F) c= A /\ (less_dom (f,+infty)) by TARSKI:def_3; hence A /\ (less_dom (f,+infty)) = union (rng F) by A12, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th25: :: MESFUNC1:25 for X being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (- n)))) ) holds A /\ (eq_dom (f,-infty)) = meet (rng F) proof let X be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (- n)))) ) holds A /\ (eq_dom (f,-infty)) = meet (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (- n)))) ) holds A /\ (eq_dom (f,-infty)) = meet (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (- n)))) ) holds A /\ (eq_dom (f,-infty)) = meet (rng F) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set st ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (- n)))) ) holds A /\ (eq_dom (f,-infty)) = meet (rng F) let A be set ; ::_thesis: ( ( for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (- n)))) ) implies A /\ (eq_dom (f,-infty)) = meet (rng F) ) assume A1: for n being Element of NAT holds F . n = A /\ (less_dom (f,(R_EAL (- n)))) ; ::_thesis: A /\ (eq_dom (f,-infty)) = meet (rng F) for x being set st x in A /\ (eq_dom (f,-infty)) holds x in meet (rng F) proof let x be set ; ::_thesis: ( x in A /\ (eq_dom (f,-infty)) implies x in meet (rng F) ) assume A2: x in A /\ (eq_dom (f,-infty)) ; ::_thesis: x in meet (rng F) then A3: x in A by XBOOLE_0:def_4; A4: x in eq_dom (f,-infty) by A2, XBOOLE_0:def_4; for Y being set st Y in rng F holds x in Y proof let Y be set ; ::_thesis: ( Y in rng F implies x in Y ) ( Y in rng F implies x in Y ) proof assume Y in rng F ; ::_thesis: x in Y then consider m being Element of NAT such that m in dom F and A5: Y = F . m by PARTFUN1:3; A6: Y = A /\ (less_dom (f,(R_EAL (- m)))) by A1, A5; reconsider x = x as Element of X by A2; A7: f . x = -infty by A4, Def15; ( x in dom f & not R_EAL (- m) <= -infty ) by A4, Def15, XXREAL_0:12; then x in less_dom (f,(R_EAL (- m))) by A7, Def11; hence x in Y by A3, A6, XBOOLE_0:def_4; ::_thesis: verum end; hence ( Y in rng F implies x in Y ) ; ::_thesis: verum end; hence x in meet (rng F) by SETFAM_1:def_1; ::_thesis: verum end; then A8: A /\ (eq_dom (f,-infty)) c= meet (rng F) by TARSKI:def_3; for x being set st x in meet (rng F) holds x in A /\ (eq_dom (f,-infty)) proof let x be set ; ::_thesis: ( x in meet (rng F) implies x in A /\ (eq_dom (f,-infty)) ) assume A9: x in meet (rng F) ; ::_thesis: x in A /\ (eq_dom (f,-infty)) A10: for m being Element of NAT holds ( x in A & x in dom f & ex y being R_eal st ( y = f . x & y = -infty ) ) proof let m be Element of NAT ; ::_thesis: ( x in A & x in dom f & ex y being R_eal st ( y = f . x & y = -infty ) ) m in NAT ; then m in dom F by FUNCT_2:def_1; then F . m in rng F by FUNCT_1:def_3; then x in F . m by A9, SETFAM_1:def_1; then A11: x in A /\ (less_dom (f,(R_EAL (- m)))) by A1; then A12: x in less_dom (f,(R_EAL (- m))) by XBOOLE_0:def_4; for r being Real holds f . x < R_EAL r proof let r be Real; ::_thesis: f . x < R_EAL r consider n being Element of NAT such that A13: - n <= r by Th9; n in NAT ; then n in dom F by FUNCT_2:def_1; then F . n in rng F by FUNCT_1:def_3; then x in F . n by A9, SETFAM_1:def_1; then x in A /\ (less_dom (f,(R_EAL (- n)))) by A1; then x in less_dom (f,(R_EAL (- n))) by XBOOLE_0:def_4; then f . x < R_EAL (- n) by Def11; hence f . x < R_EAL r by A13, XXREAL_0:2; ::_thesis: verum end; then f . x = -infty by Th13; hence ( x in A & x in dom f & ex y being R_eal st ( y = f . x & y = -infty ) ) by A11, A12, Def11, XBOOLE_0:def_4; ::_thesis: verum end; 1 in NAT ; then 1 in dom F by FUNCT_2:def_1; then F . 1 in rng F by FUNCT_1:def_3; then x in F . 1 by A9, SETFAM_1:def_1; then x in A /\ (less_dom (f,(R_EAL (- 1)))) by A1; then reconsider x = x as Element of X ; x in eq_dom (f,-infty) by A10, Def15; hence x in A /\ (eq_dom (f,-infty)) by A10, XBOOLE_0:def_4; ::_thesis: verum end; then meet (rng F) c= A /\ (eq_dom (f,-infty)) by TARSKI:def_3; hence A /\ (eq_dom (f,-infty)) = meet (rng F) by A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th26: :: MESFUNC1:26 for X being set for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) holds A /\ (great_dom (f,-infty)) = union (rng F) proof let X be set ; ::_thesis: for S being SigmaField of X for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) holds A /\ (great_dom (f,-infty)) = union (rng F) let S be SigmaField of X; ::_thesis: for F being Function of NAT,S for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) holds A /\ (great_dom (f,-infty)) = union (rng F) let F be Function of NAT,S; ::_thesis: for f being PartFunc of X,ExtREAL for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) holds A /\ (great_dom (f,-infty)) = union (rng F) let f be PartFunc of X,ExtREAL; ::_thesis: for A being set st ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) holds A /\ (great_dom (f,-infty)) = union (rng F) let A be set ; ::_thesis: ( ( for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ) implies A /\ (great_dom (f,-infty)) = union (rng F) ) assume A1: for n being Element of NAT holds F . n = A /\ (great_dom (f,(R_EAL (- n)))) ; ::_thesis: A /\ (great_dom (f,-infty)) = union (rng F) for x being set st x in A /\ (great_dom (f,-infty)) holds x in union (rng F) proof let x be set ; ::_thesis: ( x in A /\ (great_dom (f,-infty)) implies x in union (rng F) ) assume A2: x in A /\ (great_dom (f,-infty)) ; ::_thesis: x in union (rng F) then A3: x in A by XBOOLE_0:def_4; A4: x in great_dom (f,-infty) by A2, XBOOLE_0:def_4; then A5: x in dom f by Def13; A6: -infty < f . x by A4, Def13; ex n being Element of NAT st R_EAL (- n) < f . x proof percases ( f . x = +infty or not f . x = +infty ) ; supposeA7: f . x = +infty ; ::_thesis: ex n being Element of NAT st R_EAL (- n) < f . x take 0 ; ::_thesis: R_EAL (- 0) < f . x thus R_EAL (- 0) < f . x by A7; ::_thesis: verum end; suppose not f . x = +infty ; ::_thesis: ex n being Element of NAT st R_EAL (- n) < f . x then not +infty <= f . x by XXREAL_0:4; then reconsider y1 = f . x as Real by A6, XXREAL_0:48; consider n1 being Element of NAT such that A8: - n1 <= y1 by Th9; n1 < n1 + 1 by NAT_1:13; then A9: - (n1 + 1) < - n1 by XREAL_1:24; reconsider m = n1 + 1 as Element of NAT ; take m ; ::_thesis: R_EAL (- m) < f . x thus R_EAL (- m) < f . x by A8, A9, XXREAL_0:2; ::_thesis: verum end; end; end; then consider n being Element of NAT such that A10: R_EAL (- n) < f . x ; reconsider x = x as Element of X by A2; x in great_dom (f,(R_EAL (- n))) by A5, A10, Def13; then x in A /\ (great_dom (f,(R_EAL (- n)))) by A3, XBOOLE_0:def_4; then A11: x in F . n by A1; n in NAT ; then n in dom F by FUNCT_2:def_1; then F . n in rng F by FUNCT_1:def_3; hence x in union (rng F) by A11, TARSKI:def_4; ::_thesis: verum end; then A12: A /\ (great_dom (f,-infty)) c= union (rng F) by TARSKI:def_3; for x being set st x in union (rng F) holds x in A /\ (great_dom (f,-infty)) proof let x be set ; ::_thesis: ( x in union (rng F) implies x in A /\ (great_dom (f,-infty)) ) assume x in union (rng F) ; ::_thesis: x in A /\ (great_dom (f,-infty)) then consider Y being set such that A13: x in Y and A14: Y in rng F by TARSKI:def_4; consider m being Element of NAT such that m in dom F and A15: F . m = Y by A14, PARTFUN1:3; A16: x in A /\ (great_dom (f,(R_EAL (- m)))) by A1, A13, A15; then A17: x in A by XBOOLE_0:def_4; A18: x in great_dom (f,(R_EAL (- m))) by A16, XBOOLE_0:def_4; then A19: x in dom f by Def13; A20: R_EAL (- m) < f . x by A18, Def13; reconsider x = x as Element of X by A13, A14; -infty < f . x by A20, XXREAL_0:2, XXREAL_0:12; then x in great_dom (f,-infty) by A19, Def13; hence x in A /\ (great_dom (f,-infty)) by A17, XBOOLE_0:def_4; ::_thesis: verum end; then union (rng F) c= A /\ (great_dom (f,-infty)) by TARSKI:def_3; hence A /\ (great_dom (f,-infty)) = union (rng F) by A12, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let X be non empty set ; let S be SigmaField of X; let f be PartFunc of X,ExtREAL; let A be Element of S; predf is_measurable_on A means :Def16: :: MESFUNC1:def 16 for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S; end; :: deftheorem Def16 defines is_measurable_on MESFUNC1:def_16_:_ for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S ); theorem :: MESFUNC1:27 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) let A be Element of S; ::_thesis: ( A c= dom f implies ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) ) assume A1: A c= dom f ; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) A2: ( f is_measurable_on A implies for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) proof assume A3: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (great_eq_dom (f,(R_EAL r))) in S ( A /\ (less_dom (f,(R_EAL r))) in S & A /\ (great_eq_dom (f,(R_EAL r))) = A \ (A /\ (less_dom (f,(R_EAL r)))) ) by A1, A3, Def16, Th14; hence A /\ (great_eq_dom (f,(R_EAL r))) in S by MEASURE1:6; ::_thesis: verum end; hence for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ; ::_thesis: verum end; ( ( for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) implies f is_measurable_on A ) proof assume A4: for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ; ::_thesis: f is_measurable_on A for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (less_dom (f,(R_EAL r))) in S ( A /\ (great_eq_dom (f,(R_EAL r))) in S & A /\ (less_dom (f,(R_EAL r))) = A \ (A /\ (great_eq_dom (f,(R_EAL r)))) ) by A1, A4, Th17; hence A /\ (less_dom (f,(R_EAL r))) in S by MEASURE1:6; ::_thesis: verum end; hence f is_measurable_on A by Def16; ::_thesis: verum end; hence ( f is_measurable_on A iff for r being real number holds A /\ (great_eq_dom (f,(R_EAL r))) in S ) by A2; ::_thesis: verum end; theorem Th28: :: MESFUNC1:28 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ) let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S holds ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ) let A be Element of S; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ) A1: ( f is_measurable_on A implies for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ) proof assume A2: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (less_eq_dom (f,(R_EAL r))) in S defpred S1[ Element of NAT , set ] means A /\ (less_dom (f,(R_EAL (r + (1 / (\$1 + 1)))))) = \$2; A3: for n being Element of NAT ex y being Element of S st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of S st S1[n,y] reconsider y = A /\ (less_dom (f,(R_EAL (r + (1 / (n + 1)))))) as Element of S by A2, Def16; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; consider F being Function of NAT,S such that A4: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A3); A /\ (less_eq_dom (f,(R_EAL r))) = meet (rng F) by A4, Th20; hence A /\ (less_eq_dom (f,(R_EAL r))) in S ; ::_thesis: verum end; hence for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ; ::_thesis: verum end; ( ( for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ) implies f is_measurable_on A ) proof assume A5: for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ; ::_thesis: f is_measurable_on A for r being real number holds A /\ (less_dom (f,(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (less_dom (f,(R_EAL r))) in S defpred S1[ Element of NAT , set ] means A /\ (less_eq_dom (f,(R_EAL (r - (1 / (\$1 + 1)))))) = \$2; A6: for n being Element of NAT ex y being Element of S st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of S st S1[n,y] reconsider y = A /\ (less_eq_dom (f,(R_EAL (r - (1 / (n + 1)))))) as Element of S by A5; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; consider F being Function of NAT,S such that A7: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A6); A /\ (less_dom (f,(R_EAL r))) = union (rng F) by A7, Th21; hence A /\ (less_dom (f,(R_EAL r))) in S ; ::_thesis: verum end; hence f is_measurable_on A by Def16; ::_thesis: verum end; hence ( f is_measurable_on A iff for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S ) by A1; ::_thesis: verum end; theorem Th29: :: MESFUNC1:29 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st A c= dom f holds ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) let A be Element of S; ::_thesis: ( A c= dom f implies ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) ) assume A1: A c= dom f ; ::_thesis: ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) A2: ( f is_measurable_on A implies for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) proof assume A3: f is_measurable_on A ; ::_thesis: for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (great_dom (f,(R_EAL r))) in S ( A /\ (less_eq_dom (f,(R_EAL r))) in S & A /\ (great_dom (f,(R_EAL r))) = A \ (A /\ (less_eq_dom (f,(R_EAL r)))) ) by A1, A3, Th15, Th28; hence A /\ (great_dom (f,(R_EAL r))) in S by MEASURE1:6; ::_thesis: verum end; hence for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ; ::_thesis: verum end; ( ( for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) implies f is_measurable_on A ) proof assume A4: for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ; ::_thesis: f is_measurable_on A for r being real number holds A /\ (less_eq_dom (f,(R_EAL r))) in S proof let r be real number ; ::_thesis: A /\ (less_eq_dom (f,(R_EAL r))) in S ( A /\ (great_dom (f,(R_EAL r))) in S & A /\ (less_eq_dom (f,(R_EAL r))) = A \ (A /\ (great_dom (f,(R_EAL r)))) ) by A1, A4, Th16; hence A /\ (less_eq_dom (f,(R_EAL r))) in S by MEASURE1:6; ::_thesis: verum end; hence f is_measurable_on A by Th28; ::_thesis: verum end; hence ( f is_measurable_on A iff for r being real number holds A /\ (great_dom (f,(R_EAL r))) in S ) by A2; ::_thesis: verum end; theorem :: MESFUNC1:30 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A, B being Element of S st B c= A & f is_measurable_on A holds f is_measurable_on B proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A, B being Element of S st B c= A & f is_measurable_on A holds f is_measurable_on B let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A, B being Element of S st B c= A & f is_measurable_on A holds f is_measurable_on B let f be PartFunc of X,ExtREAL; ::_thesis: for A, B being Element of S st B c= A & f is_measurable_on A holds f is_measurable_on B let A, B be Element of S; ::_thesis: ( B c= A & f is_measurable_on A implies f is_measurable_on B ) assume that A1: B c= A and A2: f is_measurable_on A ; ::_thesis: f is_measurable_on B for r being real number holds B /\ (less_dom (f,(R_EAL r))) in S proof let r be real number ; ::_thesis: B /\ (less_dom (f,(R_EAL r))) in S A3: A /\ (less_dom (f,(R_EAL r))) in S by A2, Def16; B /\ (A /\ (less_dom (f,(R_EAL r)))) = (B /\ A) /\ (less_dom (f,(R_EAL r))) by XBOOLE_1:16 .= B /\ (less_dom (f,(R_EAL r))) by A1, XBOOLE_1:28 ; hence B /\ (less_dom (f,(R_EAL r))) in S by A3, FINSUB_1:def_2; ::_thesis: verum end; hence f is_measurable_on B by Def16; ::_thesis: verum end; theorem :: MESFUNC1:31 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds f is_measurable_on A \/ B proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds f is_measurable_on A \/ B let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds f is_measurable_on A \/ B let f be PartFunc of X,ExtREAL; ::_thesis: for A, B being Element of S st f is_measurable_on A & f is_measurable_on B holds f is_measurable_on A \/ B let A, B be Element of S; ::_thesis: ( f is_measurable_on A & f is_measurable_on B implies f is_measurable_on A \/ B ) assume A1: ( f is_measurable_on A & f is_measurable_on B ) ; ::_thesis: f is_measurable_on A \/ B for r being real number holds (A \/ B) /\ (less_dom (f,(R_EAL r))) in S proof let r be real number ; ::_thesis: (A \/ B) /\ (less_dom (f,(R_EAL r))) in S ( A /\ (less_dom (f,(R_EAL r))) in S & B /\ (less_dom (f,(R_EAL r))) in S ) by A1, Def16; then (A /\ (less_dom (f,(R_EAL r)))) \/ (B /\ (less_dom (f,(R_EAL r)))) in S by FINSUB_1:def_1; hence (A \/ B) /\ (less_dom (f,(R_EAL r))) in S by XBOOLE_1:23; ::_thesis: verum end; hence f is_measurable_on A \/ B by Def16; ::_thesis: verum end; theorem :: MESFUNC1:32 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S let A be Element of S; ::_thesis: for r, s being Real st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S let r, s be Real; ::_thesis: ( f is_measurable_on A & A c= dom f implies (A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: (A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S A3: A /\ (less_dom (f,(R_EAL s))) in S by A1, Def16; A4: for r1 being Real holds A /\ (great_eq_dom (f,(R_EAL r1))) in S proof let r1 be Real; ::_thesis: A /\ (great_eq_dom (f,(R_EAL r1))) in S ( A /\ (less_dom (f,(R_EAL r1))) in S & A /\ (great_eq_dom (f,(R_EAL r1))) = A \ (A /\ (less_dom (f,(R_EAL r1)))) ) by A1, A2, Def16, Th14; hence A /\ (great_eq_dom (f,(R_EAL r1))) in S by MEASURE1:6; ::_thesis: verum end; for r1 being Real holds A /\ (great_dom (f,(R_EAL r1))) in S proof let r1 be Real; ::_thesis: A /\ (great_dom (f,(R_EAL r1))) in S defpred S1[ Element of NAT , set ] means A /\ (great_eq_dom (f,(R_EAL (r1 + (1 / (\$1 + 1)))))) = \$2; A5: for n being Element of NAT ex y being Element of S st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of S st S1[n,y] reconsider y = A /\ (great_eq_dom (f,(R_EAL (r1 + (1 / (n + 1)))))) as Element of S by A4; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; consider F being Function of NAT,S such that A6: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A5); A /\ (great_dom (f,(R_EAL r1))) = union (rng F) by A6, Th22; hence A /\ (great_dom (f,(R_EAL r1))) in S ; ::_thesis: verum end; then A7: A /\ (great_dom (f,(R_EAL r))) in S ; (A /\ (great_dom (f,(R_EAL r)))) /\ (A /\ (less_dom (f,(R_EAL s)))) = ((A /\ (great_dom (f,(R_EAL r)))) /\ A) /\ (less_dom (f,(R_EAL s))) by XBOOLE_1:16 .= ((great_dom (f,(R_EAL r))) /\ (A /\ A)) /\ (less_dom (f,(R_EAL s))) by XBOOLE_1:16 ; hence (A /\ (great_dom (f,(R_EAL r)))) /\ (less_dom (f,(R_EAL s))) in S by A3, A7, FINSUB_1:def_2; ::_thesis: verum end; theorem :: MESFUNC1:33 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds A /\ (eq_dom (f,+infty)) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds A /\ (eq_dom (f,+infty)) in S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds A /\ (eq_dom (f,+infty)) in S let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds A /\ (eq_dom (f,+infty)) in S let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies A /\ (eq_dom (f,+infty)) in S ) assume A1: ( f is_measurable_on A & A c= dom f ) ; ::_thesis: A /\ (eq_dom (f,+infty)) in S defpred S1[ Element of NAT , set ] means A /\ (great_dom (f,(R_EAL \$1))) = \$2; A2: for n being Element of NAT ex y being Element of S st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of S st S1[n,y] reconsider y = A /\ (great_dom (f,(R_EAL n))) as Element of S by A1, Th29; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; consider F being Function of NAT,S such that A3: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A2); A /\ (eq_dom (f,+infty)) = meet (rng F) by A3, Th23; hence A /\ (eq_dom (f,+infty)) in S ; ::_thesis: verum end; theorem :: MESFUNC1:34 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A holds A /\ (eq_dom (f,-infty)) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A holds A /\ (eq_dom (f,-infty)) in S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A holds A /\ (eq_dom (f,-infty)) in S let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is_measurable_on A holds A /\ (eq_dom (f,-infty)) in S let A be Element of S; ::_thesis: ( f is_measurable_on A implies A /\ (eq_dom (f,-infty)) in S ) assume A1: f is_measurable_on A ; ::_thesis: A /\ (eq_dom (f,-infty)) in S defpred S1[ Element of NAT , set ] means A /\ (less_dom (f,(R_EAL (- \$1)))) = \$2; A2: for n being Element of NAT ex y being Element of S st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of S st S1[n,y] reconsider y = A /\ (less_dom (f,(R_EAL (- n)))) as Element of S by A1, Def16; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; consider F being Function of NAT,S such that A3: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A2); A /\ (eq_dom (f,-infty)) = meet (rng F) by A3, Th25; hence A /\ (eq_dom (f,-infty)) in S ; ::_thesis: verum end; theorem :: MESFUNC1:35 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,-infty))) /\ (less_dom (f,+infty)) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,-infty))) /\ (less_dom (f,+infty)) in S let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,-infty))) /\ (less_dom (f,+infty)) in S let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S st f is_measurable_on A & A c= dom f holds (A /\ (great_dom (f,-infty))) /\ (less_dom (f,+infty)) in S let A be Element of S; ::_thesis: ( f is_measurable_on A & A c= dom f implies (A /\ (great_dom (f,-infty))) /\ (less_dom (f,+infty)) in S ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: (A /\ (great_dom (f,-infty))) /\ (less_dom (f,+infty)) in S A3: A /\ (great_dom (f,-infty)) in S proof defpred S1[ Element of NAT , set ] means A /\ (great_dom (f,(R_EAL (- \$1)))) = \$2; A4: for n being Element of NAT ex y being Element of S st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of S st S1[n,y] reconsider y = A /\ (great_dom (f,(R_EAL (- n)))) as Element of S by A1, A2, Th29; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; consider F being Function of NAT,S such that A5: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A4); A /\ (great_dom (f,-infty)) = union (rng F) by A5, Th26; hence A /\ (great_dom (f,-infty)) in S ; ::_thesis: verum end; A6: A /\ (less_dom (f,+infty)) in S proof defpred S1[ Element of NAT , set ] means A /\ (less_dom (f,(R_EAL \$1))) = \$2; A7: for n being Element of NAT ex y being Element of S st S1[n,y] proof let n be Element of NAT ; ::_thesis: ex y being Element of S st S1[n,y] reconsider y = A /\ (less_dom (f,(R_EAL n))) as Element of S by A1, Def16; take y ; ::_thesis: S1[n,y] thus S1[n,y] ; ::_thesis: verum end; consider F being Function of NAT,S such that A8: for n being Element of NAT holds S1[n,F . n] from FUNCT_2:sch_3(A7); A /\ (less_dom (f,+infty)) = union (rng F) by A8, Th24; hence A /\ (less_dom (f,+infty)) in S ; ::_thesis: verum end; (A /\ (great_dom (f,-infty))) /\ (A /\ (less_dom (f,+infty))) = ((A /\ (great_dom (f,-infty))) /\ A) /\ (less_dom (f,+infty)) by XBOOLE_1:16 .= ((great_dom (f,-infty)) /\ (A /\ A)) /\ (less_dom (f,+infty)) by XBOOLE_1:16 ; hence (A /\ (great_dom (f,-infty))) /\ (less_dom (f,+infty)) in S by A3, A6, FINSUB_1:def_2; ::_thesis: verum end; theorem :: MESFUNC1:36 for X being non empty set for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f, g being PartFunc of X,ExtREAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S let S be SigmaField of X; ::_thesis: for f, g being PartFunc of X,ExtREAL for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S let f, g be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S let A be Element of S; ::_thesis: for r being Real st f is_measurable_on A & g is_measurable_on A & A c= dom g holds (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S let r be Real; ::_thesis: ( f is_measurable_on A & g is_measurable_on A & A c= dom g implies (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S ) assume ( f is_measurable_on A & g is_measurable_on A & A c= dom g ) ; ::_thesis: (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S then A1: ( A /\ (less_dom (f,(R_EAL r))) in S & A /\ (great_dom (g,(R_EAL r))) in S ) by Def16, Th29; (A /\ (less_dom (f,(R_EAL r)))) /\ (A /\ (great_dom (g,(R_EAL r)))) = ((A /\ (less_dom (f,(R_EAL r)))) /\ A) /\ (great_dom (g,(R_EAL r))) by XBOOLE_1:16 .= ((A /\ A) /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) by XBOOLE_1:16 .= (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) ; hence (A /\ (less_dom (f,(R_EAL r)))) /\ (great_dom (g,(R_EAL r))) in S by A1, FINSUB_1:def_2; ::_thesis: verum end; theorem :: MESFUNC1:37 for X being non empty set for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A proof let X be non empty set ; ::_thesis: for S being SigmaField of X for f being PartFunc of X,ExtREAL for A being Element of S for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A let S be SigmaField of X; ::_thesis: for f being PartFunc of X,ExtREAL for A being Element of S for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A let f be PartFunc of X,ExtREAL; ::_thesis: for A being Element of S for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A let A be Element of S; ::_thesis: for r being Real st f is_measurable_on A & A c= dom f holds r (#) f is_measurable_on A let r be Real; ::_thesis: ( f is_measurable_on A & A c= dom f implies r (#) f is_measurable_on A ) assume that A1: f is_measurable_on A and A2: A c= dom f ; ::_thesis: r (#) f is_measurable_on A for r1 being real number holds A /\ (less_dom ((r (#) f),(R_EAL r1))) in S proof let r1 be real number ; ::_thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S now__::_thesis:_A_/\_(less_dom_((r_(#)_f),(R_EAL_r1)))_in_S percases ( r <> 0 or r = 0 ) ; supposeA3: r <> 0 ; ::_thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S A4: r1 in REAL by XREAL_0:def_1; reconsider r0 = r1 / r as Real ; A5: r1 = r * r0 by A3, XCMPLX_1:87; now__::_thesis:_A_/\_(less_dom_((r_(#)_f),(R_EAL_r1)))_in_S percases ( r > 0 or r < 0 ) by A3; supposeA6: r > 0 ; ::_thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S for x being Element of X st x in less_dom (f,(R_EAL r0)) holds x in less_dom ((r (#) f),(R_EAL r1)) proof let x be Element of X; ::_thesis: ( x in less_dom (f,(R_EAL r0)) implies x in less_dom ((r (#) f),(R_EAL r1)) ) assume A7: x in less_dom (f,(R_EAL r0)) ; ::_thesis: x in less_dom ((r (#) f),(R_EAL r1)) then x in dom f by Def11; then A8: x in dom (r (#) f) by Def6; A9: f . x < R_EAL r0 by A7, Def11; A10: r1 in REAL by XREAL_0:def_1; then f . x < (R_EAL r1) / (R_EAL r) by A9, EXTREAL1:6; then A11: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A6, XXREAL_3:72; (R_EAL r1) / (R_EAL r) = r1 / r by A10, EXTREAL1:2; then A12: ((R_EAL r1) / (R_EAL r)) * (R_EAL r) = (r1 / r) * r by EXTREAL1:1 .= r1 / (r / r) by XCMPLX_1:81 .= r1 / 1 by A3, XCMPLX_1:60 .= r1 ; (r (#) f) . x = (R_EAL r) * (f . x) by A8, Def6; hence x in less_dom ((r (#) f),(R_EAL r1)) by A8, A11, A12, Def11; ::_thesis: verum end; then A13: less_dom (f,(R_EAL r0)) c= less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:2; for x being Element of X st x in less_dom ((r (#) f),(R_EAL r1)) holds x in less_dom (f,(R_EAL r0)) proof let x be Element of X; ::_thesis: ( x in less_dom ((r (#) f),(R_EAL r1)) implies x in less_dom (f,(R_EAL r0)) ) assume A14: x in less_dom ((r (#) f),(R_EAL r1)) ; ::_thesis: x in less_dom (f,(R_EAL r0)) then A15: x in dom (r (#) f) by Def11; (r (#) f) . x < R_EAL r1 by A14, Def11; then (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A5, EXTREAL1:5; then A16: ((r (#) f) . x) / (R_EAL r) < ((R_EAL r) * (R_EAL r0)) / (R_EAL r) by A6, XXREAL_3:80; (R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:1; then A17: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) = (r * r0) / r by EXTREAL1:2 .= r0 / (r / r) by XCMPLX_1:77 .= r0 / 1 by A3, XCMPLX_1:60 .= r0 ; ( x in dom f & f . x = ((r (#) f) . x) / (R_EAL r) ) by A3, A15, Def6, Th6; hence x in less_dom (f,(R_EAL r0)) by A16, A17, Def11; ::_thesis: verum end; then less_dom ((r (#) f),(R_EAL r1)) c= less_dom (f,(R_EAL r0)) by SUBSET_1:2; then less_dom (f,(R_EAL r0)) = less_dom ((r (#) f),(R_EAL r1)) by A13, XBOOLE_0:def_10; hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S by A1, Def16; ::_thesis: verum end; supposeA18: r < 0 ; ::_thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S for x being Element of X st x in great_dom (f,(R_EAL r0)) holds x in less_dom ((r (#) f),(R_EAL r1)) proof let x be Element of X; ::_thesis: ( x in great_dom (f,(R_EAL r0)) implies x in less_dom ((r (#) f),(R_EAL r1)) ) assume A19: x in great_dom (f,(R_EAL r0)) ; ::_thesis: x in less_dom ((r (#) f),(R_EAL r1)) then x in dom f by Def13; then A20: x in dom (r (#) f) by Def6; R_EAL r0 < f . x by A19, Def13; then (R_EAL r1) / (R_EAL r) < f . x by A4, EXTREAL1:6; then A21: (f . x) * (R_EAL r) < ((R_EAL r1) / (R_EAL r)) * (R_EAL r) by A18, XXREAL_3:102; (R_EAL r1) / (R_EAL r) = r1 / r by A4, EXTREAL1:2; then A22: ((R_EAL r1) / (R_EAL r)) * (R_EAL r) = (r1 / r) * r by EXTREAL1:1 .= r1 / (r / r) by XCMPLX_1:81 .= r1 / 1 by A3, XCMPLX_1:60 .= r1 ; (r (#) f) . x = (R_EAL r) * (f . x) by A20, Def6; hence x in less_dom ((r (#) f),(R_EAL r1)) by A20, A21, A22, Def11; ::_thesis: verum end; then A23: great_dom (f,(R_EAL r0)) c= less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:2; for x being Element of X st x in less_dom ((r (#) f),(R_EAL r1)) holds x in great_dom (f,(R_EAL r0)) proof let x be Element of X; ::_thesis: ( x in less_dom ((r (#) f),(R_EAL r1)) implies x in great_dom (f,(R_EAL r0)) ) assume A24: x in less_dom ((r (#) f),(R_EAL r1)) ; ::_thesis: x in great_dom (f,(R_EAL r0)) then A25: x in dom (r (#) f) by Def11; (r (#) f) . x < R_EAL r1 by A24, Def11; then (r (#) f) . x < (R_EAL r) * (R_EAL r0) by A5, EXTREAL1:5; then A26: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) < ((r (#) f) . x) / (R_EAL r) by A18, XXREAL_3:104; (R_EAL r) * (R_EAL r0) = r * r0 by EXTREAL1:1; then A27: ((R_EAL r) * (R_EAL r0)) / (R_EAL r) = (r * r0) / r by EXTREAL1:2 .= r0 / (r / r) by XCMPLX_1:77 .= r0 / 1 by A3, XCMPLX_1:60 .= r0 ; ( x in dom f & f . x = ((r (#) f) . x) / (R_EAL r) ) by A3, A25, Def6, Th6; hence x in great_dom (f,(R_EAL r0)) by A26, A27, Def13; ::_thesis: verum end; then less_dom ((r (#) f),(R_EAL r1)) c= great_dom (f,(R_EAL r0)) by SUBSET_1:2; then great_dom (f,(R_EAL r0)) = less_dom ((r (#) f),(R_EAL r1)) by A23, XBOOLE_0:def_10; hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S by A1, A2, Th29; ::_thesis: verum end; end; end; hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S ; ::_thesis: verum end; supposeA28: r = 0 ; ::_thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S now__::_thesis:_A_/\_(less_dom_((r_(#)_f),(R_EAL_r1)))_in_S percases ( r1 > 0 or r1 <= 0 ) ; supposeA29: r1 > 0 ; ::_thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S for x1 being set st x1 in A holds x1 in A /\ (less_dom ((r (#) f),(R_EAL r1))) proof let x1 be set ; ::_thesis: ( x1 in A implies x1 in A /\ (less_dom ((r (#) f),(R_EAL r1))) ) assume A30: x1 in A ; ::_thesis: x1 in A /\ (less_dom ((r (#) f),(R_EAL r1))) then reconsider x1 = x1 as Element of X ; x1 in dom f by A2, A30; then A31: x1 in dom (r (#) f) by Def6; reconsider y = (r (#) f) . x1 as R_eal ; y = (R_EAL r) * (f . x1) by A31, Def6 .= 0. by A28 ; then x1 in less_dom ((r (#) f),(R_EAL r1)) by A29, A31, Def11; hence x1 in A /\ (less_dom ((r (#) f),(R_EAL r1))) by A30, XBOOLE_0:def_4; ::_thesis: verum end; then ( A /\ (less_dom ((r (#) f),(R_EAL r1))) c= A & A c= A /\ (less_dom ((r (#) f),(R_EAL r1))) ) by TARSKI:def_3, XBOOLE_1:17; then A /\ (less_dom ((r (#) f),(R_EAL r1))) = A by XBOOLE_0:def_10; hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S ; ::_thesis: verum end; supposeA32: r1 <= 0 ; ::_thesis: A /\ (less_dom ((r (#) f),(R_EAL r1))) in S less_dom ((r (#) f),(R_EAL r1)) = {} proof assume less_dom ((r (#) f),(R_EAL r1)) <> {} ; ::_thesis: contradiction then consider x1 being Element of X such that A33: x1 in less_dom ((r (#) f),(R_EAL r1)) by SUBSET_1:4; A34: x1 in dom (r (#) f) by A33, Def11; A35: (r (#) f) . x1 < R_EAL r1 by A33, Def11; A36: (r (#) f) . x1 in rng (r (#) f) by A34, FUNCT_1:def_3; for y being R_eal st y in rng (r (#) f) holds not y < R_EAL r1 proof let y be R_eal; ::_thesis: ( y in rng (r (#) f) implies not y < R_EAL r1 ) assume y in rng (r (#) f) ; ::_thesis: not y < R_EAL r1 then consider x being Element of X such that A37: ( x in dom (r (#) f) & y = (r (#) f) . x ) by PARTFUN1:3; y = (R_EAL r) * (f . x) by A37, Def6 .= 0. by A28 ; hence not y < R_EAL r1 by A32; ::_thesis: verum end; hence contradiction by A35, A36; ::_thesis: verum end; hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S by PROB_1:4; ::_thesis: verum end; end; end; hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S ; ::_thesis: verum end; end; end; hence A /\ (less_dom ((r (#) f),(R_EAL r1))) in S ; ::_thesis: verum end; hence r (#) f is_measurable_on A by Def16; ::_thesis: verum end;