:: 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;