:: MESFUNC1 semantic presentation

definition
func INT- -> Subset of REAL means :Def1: :: MESFUNC1:def 1
for b1 being Real holds
( b1 in a1 iff ex b2 being Nat st b1 = - b2 );
existence
ex b1 being Subset of REAL st
for b2 being Real holds
( b2 in b1 iff ex b3 being Nat st b2 = - b3 )
proof end;
uniqueness
for b1, b2 being Subset of REAL st ( for b3 being Real holds
( b3 in b1 iff ex b4 being Nat st b3 = - b4 ) ) & ( for b3 being Real holds
( b3 in b2 iff ex b4 being Nat st b3 = - b4 ) ) holds
b1 = b2
proof end;
correctness
;
end;

:: deftheorem Def1 defines INT- MESFUNC1:def 1 :
for b1 being Subset of REAL holds
( b1 = INT- iff for b2 being Real holds
( b2 in b1 iff ex b3 being Nat st b2 = - b3 ) );

Lemma2: 0 = - 0
;

registration
cluster INT- -> non empty ;
coherence
not INT- is empty by Def1, Lemma2;
end;

theorem Th1: :: MESFUNC1:1
NAT , INT- are_equipotent
proof end;

theorem Th2: :: MESFUNC1:2
INT = INT- \/ NAT
proof end;

theorem Th3: :: MESFUNC1:3
NAT , INT are_equipotent by Th1, Th2, CARD_4:15, CARD_4:35;

definition
redefine func INT as INT -> Subset of REAL ;
correctness
coherence
INT is Subset of REAL ;
by NUMBERS:15;
end;

definition
let c1 be Nat;
func RAT_with_denominator c1 -> Subset of RAT means :Def2: :: MESFUNC1:def 2
for b1 being Rational holds
( b1 in a2 iff ex b2 being Integer st b1 = b2 / a1 );
existence
ex b1 being Subset of RAT st
for b2 being Rational holds
( b2 in b1 iff ex b3 being Integer st b2 = b3 / c1 )
proof end;
uniqueness
for b1, b2 being Subset of RAT st ( for b3 being Rational holds
( b3 in b1 iff ex b4 being Integer st b3 = b4 / c1 ) ) & ( for b3 being Rational holds
( b3 in b2 iff ex b4 being Integer st b3 = b4 / c1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines RAT_with_denominator MESFUNC1:def 2 :
for b1 being Nat
for b2 being Subset of RAT holds
( b2 = RAT_with_denominator b1 iff for b3 being Rational holds
( b3 in b2 iff ex b4 being Integer st b3 = b4 / b1 ) );

registration
let c1 be Nat;
cluster RAT_with_denominator (a1 + 1) -> non empty ;
coherence
not RAT_with_denominator (c1 + 1) is empty
proof end;
end;

theorem Th4: :: MESFUNC1:4
for b1 being Nat holds INT , RAT_with_denominator (b1 + 1) are_equipotent
proof end;

theorem Th5: :: MESFUNC1:5
NAT , RAT are_equipotent
proof end;

definition
let c1 be non empty set ;
let c2 be PartFunc of c1, ExtREAL ;
let c3 be set ;
redefine func . as c2 . c3 -> R_eal;
coherence
c2 . c3 is R_eal
proof end;
end;

definition
let c1 be non empty set ;
let c2, c3 be PartFunc of c1, ExtREAL ;
deffunc H1( Element of c1) -> Element of ExtREAL = (c2 . a1) + (c3 . a1);
func c2 + c3 -> PartFunc of a1, ExtREAL means :Def3: :: MESFUNC1:def 3
( dom a4 = ((dom a2) /\ (dom a3)) \ (((a2 " {-infty }) /\ (a3 " {+infty })) \/ ((a2 " {+infty }) /\ (a3 " {-infty }))) & ( for b1 being Element of a1 st b1 in dom a4 holds
a4 . b1 = (a2 . b1) + (a3 . b1) ) );
existence
ex b1 being PartFunc of c1, ExtREAL st
( dom b1 = ((dom c2) /\ (dom c3)) \ (((c2 " {-infty }) /\ (c3 " {+infty })) \/ ((c2 " {+infty }) /\ (c3 " {-infty }))) & ( for b2 being Element of c1 st b2 in dom b1 holds
b1 . b2 = (c2 . b2) + (c3 . b2) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of c1, ExtREAL st dom b1 = ((dom c2) /\ (dom c3)) \ (((c2 " {-infty }) /\ (c3 " {+infty })) \/ ((c2 " {+infty }) /\ (c3 " {-infty }))) & ( for b3 being Element of c1 st b3 in dom b1 holds
b1 . b3 = (c2 . b3) + (c3 . b3) ) & dom b2 = ((dom c2) /\ (dom c3)) \ (((c2 " {-infty }) /\ (c3 " {+infty })) \/ ((c2 " {+infty }) /\ (c3 " {-infty }))) & ( for b3 being Element of c1 st b3 in dom b2 holds
b2 . b3 = (c2 . b3) + (c3 . b3) ) holds
b1 = b2
proof end;
deffunc H2( Element of c1) -> Element of ExtREAL = (c2 . a1) - (c3 . a1);
func c2 - c3 -> PartFunc of a1, ExtREAL means :: MESFUNC1:def 4
( dom a4 = ((dom a2) /\ (dom a3)) \ (((a2 " {+infty }) /\ (a3 " {+infty })) \/ ((a2 " {-infty }) /\ (a3 " {-infty }))) & ( for b1 being Element of a1 st b1 in dom a4 holds
a4 . b1 = (a2 . b1) - (a3 . b1) ) );
existence
ex b1 being PartFunc of c1, ExtREAL st
( dom b1 = ((dom c2) /\ (dom c3)) \ (((c2 " {+infty }) /\ (c3 " {+infty })) \/ ((c2 " {-infty }) /\ (c3 " {-infty }))) & ( for b2 being Element of c1 st b2 in dom b1 holds
b1 . b2 = (c2 . b2) - (c3 . b2) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of c1, ExtREAL st dom b1 = ((dom c2) /\ (dom c3)) \ (((c2 " {+infty }) /\ (c3 " {+infty })) \/ ((c2 " {-infty }) /\ (c3 " {-infty }))) & ( for b3 being Element of c1 st b3 in dom b1 holds
b1 . b3 = (c2 . b3) - (c3 . b3) ) & dom b2 = ((dom c2) /\ (dom c3)) \ (((c2 " {+infty }) /\ (c3 " {+infty })) \/ ((c2 " {-infty }) /\ (c3 " {-infty }))) & ( for b3 being Element of c1 st b3 in dom b2 holds
b2 . b3 = (c2 . b3) - (c3 . b3) ) holds
b1 = b2
proof end;
deffunc H3( Element of c1) -> Element of ExtREAL = (c2 . a1) * (c3 . a1);
func c2 (#) c3 -> PartFunc of a1, ExtREAL means :Def5: :: MESFUNC1:def 5
( dom a4 = (dom a2) /\ (dom a3) & ( for b1 being Element of a1 st b1 in dom a4 holds
a4 . b1 = (a2 . b1) * (a3 . b1) ) );
existence
ex b1 being PartFunc of c1, ExtREAL st
( dom b1 = (dom c2) /\ (dom c3) & ( for b2 being Element of c1 st b2 in dom b1 holds
b1 . b2 = (c2 . b2) * (c3 . b2) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of c1, ExtREAL st dom b1 = (dom c2) /\ (dom c3) & ( for b3 being Element of c1 st b3 in dom b1 holds
b1 . b3 = (c2 . b3) * (c3 . b3) ) & dom b2 = (dom c2) /\ (dom c3) & ( for b3 being Element of c1 st b3 in dom b2 holds
b2 . b3 = (c2 . b3) * (c3 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines + MESFUNC1:def 3 :
for b1 being non empty set
for b2, b3, b4 being PartFunc of b1, ExtREAL holds
( b4 = b2 + b3 iff ( dom b4 = ((dom b2) /\ (dom b3)) \ (((b2 " {-infty }) /\ (b3 " {+infty })) \/ ((b2 " {+infty }) /\ (b3 " {-infty }))) & ( for b5 being Element of b1 st b5 in dom b4 holds
b4 . b5 = (b2 . b5) + (b3 . b5) ) ) );

:: deftheorem Def4 defines - MESFUNC1:def 4 :
for b1 being non empty set
for b2, b3, b4 being PartFunc of b1, ExtREAL holds
( b4 = b2 - b3 iff ( dom b4 = ((dom b2) /\ (dom b3)) \ (((b2 " {+infty }) /\ (b3 " {+infty })) \/ ((b2 " {-infty }) /\ (b3 " {-infty }))) & ( for b5 being Element of b1 st b5 in dom b4 holds
b4 . b5 = (b2 . b5) - (b3 . b5) ) ) );

:: deftheorem Def5 defines (#) MESFUNC1:def 5 :
for b1 being non empty set
for b2, b3, b4 being PartFunc of b1, ExtREAL holds
( b4 = b2 (#) b3 iff ( dom b4 = (dom b2) /\ (dom b3) & ( for b5 being Element of b1 st b5 in dom b4 holds
b4 . b5 = (b2 . b5) * (b3 . b5) ) ) );

definition
let c1 be non empty set ;
let c2 be PartFunc of c1, ExtREAL ;
let c3 be Real;
deffunc H1( Element of c1) -> Element of ExtREAL = (R_EAL c3) * (c2 . a1);
func c3 (#) c2 -> PartFunc of a1, ExtREAL means :Def6: :: MESFUNC1:def 6
( dom a4 = dom a2 & ( for b1 being Element of a1 st b1 in dom a4 holds
a4 . b1 = (R_EAL a3) * (a2 . b1) ) );
existence
ex b1 being PartFunc of c1, ExtREAL st
( dom b1 = dom c2 & ( for b2 being Element of c1 st b2 in dom b1 holds
b1 . b2 = (R_EAL c3) * (c2 . b2) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of c1, ExtREAL st dom b1 = dom c2 & ( for b3 being Element of c1 st b3 in dom b1 holds
b1 . b3 = (R_EAL c3) * (c2 . b3) ) & dom b2 = dom c2 & ( for b3 being Element of c1 st b3 in dom b2 holds
b2 . b3 = (R_EAL c3) * (c2 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines (#) MESFUNC1:def 6 :
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being Real
for b4 being PartFunc of b1, ExtREAL holds
( b4 = b3 (#) b2 iff ( dom b4 = dom b2 & ( for b5 being Element of b1 st b5 in dom b4 holds
b4 . b5 = (R_EAL b3) * (b2 . b5) ) ) );

theorem Th6: :: MESFUNC1:6
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being Real st b3 <> 0 holds
for b4 being Element of b1 st b4 in dom (b3 (#) b2) holds
b2 . b4 = ((b3 (#) b2) . b4) / (R_EAL b3)
proof end;

definition
let c1 be non empty set ;
let c2 be PartFunc of c1, ExtREAL ;
deffunc H1( Element of c1) -> Element of ExtREAL = - (c2 . a1);
func - c2 -> PartFunc of a1, ExtREAL means :: MESFUNC1:def 7
( dom a3 = dom a2 & ( for b1 being Element of a1 st b1 in dom a3 holds
a3 . b1 = - (a2 . b1) ) );
existence
ex b1 being PartFunc of c1, ExtREAL st
( dom b1 = dom c2 & ( for b2 being Element of c1 st b2 in dom b1 holds
b1 . b2 = - (c2 . b2) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of c1, ExtREAL st dom b1 = dom c2 & ( for b3 being Element of c1 st b3 in dom b1 holds
b1 . b3 = - (c2 . b3) ) & dom b2 = dom c2 & ( for b3 being Element of c1 st b3 in dom b2 holds
b2 . b3 = - (c2 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines - MESFUNC1:def 7 :
for b1 being non empty set
for b2, b3 being PartFunc of b1, ExtREAL holds
( b3 = - b2 iff ( dom b3 = dom b2 & ( for b4 being Element of b1 st b4 in dom b3 holds
b3 . b4 = - (b2 . b4) ) ) );

definition
func 1. -> R_eal equals :: MESFUNC1:def 8
1;
correctness
coherence
1 is R_eal;
by SUPINF_1:10;
end;

:: deftheorem Def8 defines 1. MESFUNC1:def 8 :
1. = 1;

definition
let c1 be non empty set ;
let c2 be PartFunc of c1, ExtREAL ;
let c3 be Real;
deffunc H1( Element of c1) -> Element of ExtREAL = (R_EAL c3) / (c2 . a1);
func c3 / c2 -> PartFunc of a1, ExtREAL means :Def9: :: MESFUNC1:def 9
( dom a4 = (dom a2) \ (a2 " {0. }) & ( for b1 being Element of a1 st b1 in dom a4 holds
a4 . b1 = (R_EAL a3) / (a2 . b1) ) );
existence
ex b1 being PartFunc of c1, ExtREAL st
( dom b1 = (dom c2) \ (c2 " {0. }) & ( for b2 being Element of c1 st b2 in dom b1 holds
b1 . b2 = (R_EAL c3) / (c2 . b2) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of c1, ExtREAL st dom b1 = (dom c2) \ (c2 " {0. }) & ( for b3 being Element of c1 st b3 in dom b1 holds
b1 . b3 = (R_EAL c3) / (c2 . b3) ) & dom b2 = (dom c2) \ (c2 " {0. }) & ( for b3 being Element of c1 st b3 in dom b2 holds
b2 . b3 = (R_EAL c3) / (c2 . b3) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines / MESFUNC1:def 9 :
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being Real
for b4 being PartFunc of b1, ExtREAL holds
( b4 = b3 / b2 iff ( dom b4 = (dom b2) \ (b2 " {0. }) & ( for b5 being Element of b1 st b5 in dom b4 holds
b4 . b5 = (R_EAL b3) / (b2 . b5) ) ) );

theorem Th7: :: MESFUNC1:7
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL holds
( dom (1 / b2) = (dom b2) \ (b2 " {0. }) & ( for b3 being Element of b1 st b3 in dom (1 / b2) holds
(1 / b2) . b3 = 1. / (b2 . b3) ) )
proof end;

definition
let c1 be non empty set ;
let c2 be PartFunc of c1, ExtREAL ;
deffunc H1( Element of c1) -> Element of ExtREAL = |.(c2 . a1).|;
func |.c2.| -> PartFunc of a1, ExtREAL means :: MESFUNC1:def 10
( dom a3 = dom a2 & ( for b1 being Element of a1 st b1 in dom a3 holds
a3 . b1 = |.(a2 . b1).| ) );
existence
ex b1 being PartFunc of c1, ExtREAL st
( dom b1 = dom c2 & ( for b2 being Element of c1 st b2 in dom b1 holds
b1 . b2 = |.(c2 . b2).| ) )
proof end;
uniqueness
for b1, b2 being PartFunc of c1, ExtREAL st dom b1 = dom c2 & ( for b3 being Element of c1 st b3 in dom b1 holds
b1 . b3 = |.(c2 . b3).| ) & dom b2 = dom c2 & ( for b3 being Element of c1 st b3 in dom b2 holds
b2 . b3 = |.(c2 . b3).| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines |. MESFUNC1:def 10 :
for b1 being non empty set
for b2, b3 being PartFunc of b1, ExtREAL holds
( b3 = |.b2.| iff ( dom b3 = dom b2 & ( for b4 being Element of b1 st b4 in dom b3 holds
b3 . b4 = |.(b2 . b4).| ) ) );

theorem Th8: :: MESFUNC1:8
canceled;

theorem Th9: :: MESFUNC1:9
for b1 being non empty set
for b2, b3 being PartFunc of b1, ExtREAL holds b2 + b3 = b3 + b2
proof end;

theorem Th10: :: MESFUNC1:10
for b1 being non empty set
for b2, b3 being PartFunc of b1, ExtREAL holds b2 (#) b3 = b3 (#) b2
proof end;

definition
let c1 be non empty set ;
let c2, c3 be PartFunc of c1, ExtREAL ;
redefine func + as c2 + c3 -> PartFunc of a1, ExtREAL ;
commutativity
for b1, b2 being PartFunc of c1, ExtREAL holds b1 + b2 = b2 + b1 by Th9;
redefine func (#) as c2 (#) c3 -> PartFunc of a1, ExtREAL ;
commutativity
for b1, b2 being PartFunc of c1, ExtREAL holds b1 (#) b2 = b2 (#) b1 by Th10;
end;

theorem Th11: :: MESFUNC1:11
for b1 being Real ex b2 being Nat st b1 <= b2
proof end;

theorem Th12: :: MESFUNC1:12
for b1 being Real ex b2 being Nat st - b2 <= b1
proof end;

theorem Th13: :: MESFUNC1:13
for b1, b2 being real number st b1 < b2 holds
ex b3 being Nat st 1 / (b3 + 1) < b2 - b1
proof end;

theorem Th14: :: MESFUNC1:14
for b1, b2 being real number st ( for b3 being Nat holds b1 - (1 / (b3 + 1)) <= b2 ) holds
b1 <= b2
proof end;

theorem Th15: :: MESFUNC1:15
for b1 being R_eal st ( for b2 being Real holds R_EAL b2 <' b1 ) holds
b1 = +infty
proof end;

theorem Th16: :: MESFUNC1:16
for b1 being R_eal st ( for b2 being Real holds b1 <' R_EAL b2 ) holds
b1 = -infty
proof end;

definition
let c1 be set ;
let c2 be sigma_Field_Subset of c1;
let c3 be set ;
pred c3 is_measurable_on c2 means :Def11: :: MESFUNC1:def 11
a3 in a2;
end;

:: deftheorem Def11 defines is_measurable_on MESFUNC1:def 11 :
for b1 being set
for b2 being sigma_Field_Subset of b1
for b3 being set holds
( b3 is_measurable_on b2 iff b3 in b2 );

theorem Th17: :: MESFUNC1:17
for b1, b2 being set
for b3 being sigma_Field_Subset of b1 holds
( b2 is_measurable_on b3 iff for b4 being sigma_Measure of b3 holds b2 is_measurable b4 )
proof end;

definition
let c1 be non empty set ;
let c2 be PartFunc of c1, ExtREAL ;
let c3 be R_eal;
func less_dom c2,c3 -> Subset of a1 means :Def12: :: MESFUNC1:def 12
for b1 being Element of a1 holds
( b1 in a4 iff ( b1 in dom a2 & ex b2 being R_eal st
( b2 = a2 . b1 & b2 <' a3 ) ) );
existence
ex b1 being Subset of c1 st
for b2 being Element of c1 holds
( b2 in b1 iff ( b2 in dom c2 & ex b3 being R_eal st
( b3 = c2 . b2 & b3 <' c3 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of c1 st ( for b3 being Element of c1 holds
( b3 in b1 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & b4 <' c3 ) ) ) ) & ( for b3 being Element of c1 holds
( b3 in b2 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & b4 <' c3 ) ) ) ) holds
b1 = b2
proof end;
correctness
;
func less_eq_dom c2,c3 -> Subset of a1 means :Def13: :: MESFUNC1:def 13
for b1 being Element of a1 holds
( b1 in a4 iff ( b1 in dom a2 & ex b2 being R_eal st
( b2 = a2 . b1 & b2 <=' a3 ) ) );
existence
ex b1 being Subset of c1 st
for b2 being Element of c1 holds
( b2 in b1 iff ( b2 in dom c2 & ex b3 being R_eal st
( b3 = c2 . b2 & b3 <=' c3 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of c1 st ( for b3 being Element of c1 holds
( b3 in b1 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & b4 <=' c3 ) ) ) ) & ( for b3 being Element of c1 holds
( b3 in b2 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & b4 <=' c3 ) ) ) ) holds
b1 = b2
proof end;
correctness
;
func great_dom c2,c3 -> Subset of a1 means :Def14: :: MESFUNC1:def 14
for b1 being Element of a1 holds
( b1 in a4 iff ( b1 in dom a2 & ex b2 being R_eal st
( b2 = a2 . b1 & a3 <' b2 ) ) );
existence
ex b1 being Subset of c1 st
for b2 being Element of c1 holds
( b2 in b1 iff ( b2 in dom c2 & ex b3 being R_eal st
( b3 = c2 . b2 & c3 <' b3 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of c1 st ( for b3 being Element of c1 holds
( b3 in b1 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & c3 <' b4 ) ) ) ) & ( for b3 being Element of c1 holds
( b3 in b2 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & c3 <' b4 ) ) ) ) holds
b1 = b2
proof end;
correctness
;
func great_eq_dom c2,c3 -> Subset of a1 means :Def15: :: MESFUNC1:def 15
for b1 being Element of a1 holds
( b1 in a4 iff ( b1 in dom a2 & ex b2 being R_eal st
( b2 = a2 . b1 & a3 <=' b2 ) ) );
existence
ex b1 being Subset of c1 st
for b2 being Element of c1 holds
( b2 in b1 iff ( b2 in dom c2 & ex b3 being R_eal st
( b3 = c2 . b2 & c3 <=' b3 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of c1 st ( for b3 being Element of c1 holds
( b3 in b1 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & c3 <=' b4 ) ) ) ) & ( for b3 being Element of c1 holds
( b3 in b2 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & c3 <=' b4 ) ) ) ) holds
b1 = b2
proof end;
correctness
;
func eq_dom c2,c3 -> Subset of a1 means :Def16: :: MESFUNC1:def 16
for b1 being Element of a1 holds
( b1 in a4 iff ( b1 in dom a2 & ex b2 being R_eal st
( b2 = a2 . b1 & a3 = b2 ) ) );
existence
ex b1 being Subset of c1 st
for b2 being Element of c1 holds
( b2 in b1 iff ( b2 in dom c2 & ex b3 being R_eal st
( b3 = c2 . b2 & c3 = b3 ) ) )
proof end;
uniqueness
for b1, b2 being Subset of c1 st ( for b3 being Element of c1 holds
( b3 in b1 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & c3 = b4 ) ) ) ) & ( for b3 being Element of c1 holds
( b3 in b2 iff ( b3 in dom c2 & ex b4 being R_eal st
( b4 = c2 . b3 & c3 = b4 ) ) ) ) holds
b1 = b2
proof end;
correctness
;
end;

:: deftheorem Def12 defines less_dom MESFUNC1:def 12 :
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being R_eal
for b4 being Subset of b1 holds
( b4 = less_dom b2,b3 iff for b5 being Element of b1 holds
( b5 in b4 iff ( b5 in dom b2 & ex b6 being R_eal st
( b6 = b2 . b5 & b6 <' b3 ) ) ) );

:: deftheorem Def13 defines less_eq_dom MESFUNC1:def 13 :
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being R_eal
for b4 being Subset of b1 holds
( b4 = less_eq_dom b2,b3 iff for b5 being Element of b1 holds
( b5 in b4 iff ( b5 in dom b2 & ex b6 being R_eal st
( b6 = b2 . b5 & b6 <=' b3 ) ) ) );

:: deftheorem Def14 defines great_dom MESFUNC1:def 14 :
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being R_eal
for b4 being Subset of b1 holds
( b4 = great_dom b2,b3 iff for b5 being Element of b1 holds
( b5 in b4 iff ( b5 in dom b2 & ex b6 being R_eal st
( b6 = b2 . b5 & b3 <' b6 ) ) ) );

:: deftheorem Def15 defines great_eq_dom MESFUNC1:def 15 :
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being R_eal
for b4 being Subset of b1 holds
( b4 = great_eq_dom b2,b3 iff for b5 being Element of b1 holds
( b5 in b4 iff ( b5 in dom b2 & ex b6 being R_eal st
( b6 = b2 . b5 & b3 <=' b6 ) ) ) );

:: deftheorem Def16 defines eq_dom MESFUNC1:def 16 :
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being R_eal
for b4 being Subset of b1 holds
( b4 = eq_dom b2,b3 iff for b5 being Element of b1 holds
( b5 in b4 iff ( b5 in dom b2 & ex b6 being R_eal st
( b6 = b2 . b5 & b3 = b6 ) ) ) );

theorem Th18: :: MESFUNC1:18
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being set
for b4 being R_eal st b3 c= dom b2 holds
b3 /\ (great_eq_dom b2,b4) = b3 \ (b3 /\ (less_dom b2,b4))
proof end;

theorem Th19: :: MESFUNC1:19
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being set
for b4 being R_eal st b3 c= dom b2 holds
b3 /\ (great_dom b2,b4) = b3 \ (b3 /\ (less_eq_dom b2,b4))
proof end;

theorem Th20: :: MESFUNC1:20
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being set
for b4 being R_eal st b3 c= dom b2 holds
b3 /\ (less_eq_dom b2,b4) = b3 \ (b3 /\ (great_dom b2,b4))
proof end;

theorem Th21: :: MESFUNC1:21
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being set
for b4 being R_eal st b3 c= dom b2 holds
b3 /\ (less_dom b2,b4) = b3 \ (b3 /\ (great_eq_dom b2,b4))
proof end;

theorem Th22: :: MESFUNC1:22
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being set
for b4 being R_eal holds b3 /\ (eq_dom b2,b4) = (b3 /\ (great_eq_dom b2,b4)) /\ (less_eq_dom b2,b4)
proof end;

theorem Th23: :: MESFUNC1:23
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2
for b4 being PartFunc of b1, ExtREAL
for b5 being set
for b6 being Real st ( for b7 being Nat holds b3 . b7 = b5 /\ (great_dom b4,(R_EAL (b6 - (1 / (b7 + 1))))) ) holds
b5 /\ (great_eq_dom b4,(R_EAL b6)) = meet (rng b3)
proof end;

theorem Th24: :: MESFUNC1:24
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being sigma_Field_Subset of b1
for b4 being Function of NAT ,b3
for b5 being set
for b6 being real number st ( for b7 being Nat holds b4 . b7 = b5 /\ (less_dom b2,(R_EAL (b6 + (1 / (b7 + 1))))) ) holds
b5 /\ (less_eq_dom b2,(R_EAL b6)) = meet (rng b4)
proof end;

theorem Th25: :: MESFUNC1:25
for b1 being non empty set
for b2 being PartFunc of b1, ExtREAL
for b3 being sigma_Field_Subset of b1
for b4 being Function of NAT ,b3
for b5 being set
for b6 being real number st ( for b7 being Nat holds b4 . b7 = b5 /\ (less_eq_dom b2,(R_EAL (b6 - (1 / (b7 + 1))))) ) holds
b5 /\ (less_dom b2,(R_EAL b6)) = union (rng b4)
proof end;

theorem Th26: :: MESFUNC1:26
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2
for b4 being PartFunc of b1, ExtREAL
for b5 being set
for b6 being Real st ( for b7 being Nat holds b3 . b7 = b5 /\ (great_eq_dom b4,(R_EAL (b6 + (1 / (b7 + 1))))) ) holds
b5 /\ (great_dom b4,(R_EAL b6)) = union (rng b3)
proof end;

theorem Th27: :: MESFUNC1:27
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2
for b4 being PartFunc of b1, ExtREAL
for b5 being set st ( for b6 being Nat holds b3 . b6 = b5 /\ (great_dom b4,(R_EAL b6)) ) holds
b5 /\ (eq_dom b4,+infty ) = meet (rng b3)
proof end;

theorem Th28: :: MESFUNC1:28
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2
for b4 being PartFunc of b1, ExtREAL
for b5 being set st ( for b6 being Nat holds b3 . b6 = b5 /\ (less_dom b4,(R_EAL b6)) ) holds
b5 /\ (less_dom b4,+infty ) = union (rng b3)
proof end;

theorem Th29: :: MESFUNC1:29
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2
for b4 being PartFunc of b1, ExtREAL
for b5 being set st ( for b6 being Nat holds b3 . b6 = b5 /\ (less_dom b4,(R_EAL (- b6))) ) holds
b5 /\ (eq_dom b4,-infty ) = meet (rng b3)
proof end;

theorem Th30: :: MESFUNC1:30
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being Function of NAT ,b2
for b4 being PartFunc of b1, ExtREAL
for b5 being set st ( for b6 being Nat holds b3 . b6 = b5 /\ (great_dom b4,(R_EAL (- b6))) ) holds
b5 /\ (great_dom b4,-infty ) = union (rng b3)
proof end;

definition
let c1 be non empty set ;
let c2 be sigma_Field_Subset of c1;
let c3 be PartFunc of c1, ExtREAL ;
let c4 be Element of c2;
pred c3 is_measurable_on c4 means :Def17: :: MESFUNC1:def 17
for b1 being real number holds a4 /\ (less_dom a3,(R_EAL b1)) is_measurable_on a2;
end;

:: deftheorem Def17 defines is_measurable_on MESFUNC1:def 17 :
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2 holds
( b3 is_measurable_on b4 iff for b5 being real number holds b4 /\ (less_dom b3,(R_EAL b5)) is_measurable_on b2 );

theorem Th31: :: MESFUNC1:31
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2 st b4 c= dom b3 holds
( b3 is_measurable_on b4 iff for b5 being real number holds b4 /\ (great_eq_dom b3,(R_EAL b5)) is_measurable_on b2 )
proof end;

theorem Th32: :: MESFUNC1:32
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2 holds
( b3 is_measurable_on b4 iff for b5 being real number holds b4 /\ (less_eq_dom b3,(R_EAL b5)) is_measurable_on b2 )
proof end;

theorem Th33: :: MESFUNC1:33
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2 st b4 c= dom b3 holds
( b3 is_measurable_on b4 iff for b5 being real number holds b4 /\ (great_dom b3,(R_EAL b5)) is_measurable_on b2 )
proof end;

theorem Th34: :: MESFUNC1:34
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4, b5 being Element of b2 st b5 c= b4 & b3 is_measurable_on b4 holds
b3 is_measurable_on b5
proof end;

theorem Th35: :: MESFUNC1:35
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4, b5 being Element of b2 st b3 is_measurable_on b4 & b3 is_measurable_on b5 holds
b3 is_measurable_on b4 \/ b5
proof end;

theorem Th36: :: MESFUNC1:36
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2
for b5, b6 being Real st b3 is_measurable_on b4 & b4 c= dom b3 holds
(b4 /\ (great_dom b3,(R_EAL b5))) /\ (less_dom b3,(R_EAL b6)) is_measurable_on b2
proof end;

theorem Th37: :: MESFUNC1:37
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2 st b3 is_measurable_on b4 & b4 c= dom b3 holds
b4 /\ (eq_dom b3,+infty ) is_measurable_on b2
proof end;

theorem Th38: :: MESFUNC1:38
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2 st b3 is_measurable_on b4 holds
b4 /\ (eq_dom b3,-infty ) is_measurable_on b2
proof end;

theorem Th39: :: MESFUNC1:39
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2 st b3 is_measurable_on b4 & b4 c= dom b3 holds
(b4 /\ (great_dom b3,-infty )) /\ (less_dom b3,+infty ) is_measurable_on b2
proof end;

theorem Th40: :: MESFUNC1:40
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3, b4 being PartFunc of b1, ExtREAL
for b5 being Element of b2
for b6 being Real st b3 is_measurable_on b5 & b4 is_measurable_on b5 & b5 c= dom b4 holds
(b5 /\ (less_dom b3,(R_EAL b6))) /\ (great_dom b4,(R_EAL b6)) is_measurable_on b2
proof end;

theorem Th41: :: MESFUNC1:41
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Element of b2
for b5 being Real st b3 is_measurable_on b4 & b4 c= dom b3 holds
b5 (#) b3 is_measurable_on b4
proof end;