let X be non empty set ; for S being SigmaField of X
for A being Element of S
for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let S be SigmaField of X; for A being Element of S
for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let A be Element of S; for f being PartFunc of X,REAL
for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let f be PartFunc of X,REAL; for a being Real holds A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
let a be Real; A /\ (eq_dom (f,a)) = (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
now for x being object st x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) holds
x in A /\ (eq_dom (f,a))let x be
object ;
( x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) implies x in A /\ (eq_dom (f,a)) )assume A1:
x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
;
x in A /\ (eq_dom (f,a))then A2:
x in less_eq_dom (
f,
a)
by XBOOLE_0:def 4;
then A3:
x in dom f
by MESFUNC6:4;
A4:
x in A /\ (great_eq_dom (f,a))
by A1, XBOOLE_0:def 4;
then
x in great_eq_dom (
f,
a)
by XBOOLE_0:def 4;
then A5:
ex
y1 being
Real st
(
y1 = f . x &
a <= y1 )
by MESFUNC6:6;
ex
y2 being
Real st
(
y2 = f . x &
y2 <= a )
by A2, MESFUNC6:4;
then
a = f . x
by A5, XXREAL_0:1;
then A6:
x in eq_dom (
f,
a)
by A3, MESFUNC6:7;
x in A
by A4, XBOOLE_0:def 4;
hence
x in A /\ (eq_dom (f,a))
by A6, XBOOLE_0:def 4;
verum end;
then A7:
(A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) c= A /\ (eq_dom (f,a))
by TARSKI:def 3;
now for x being object st x in A /\ (eq_dom (f,a)) holds
x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))let x be
object ;
( x in A /\ (eq_dom (f,a)) implies x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a)) )assume A8:
x in A /\ (eq_dom (f,a))
;
x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))then A9:
x in A
by XBOOLE_0:def 4;
A10:
x in eq_dom (
f,
a)
by A8, XBOOLE_0:def 4;
then A11:
ex
y being
Real st
(
y = f . x &
a = y )
by MESFUNC6:7;
A12:
x in dom f
by A10, MESFUNC6:7;
then
x in great_eq_dom (
f,
a)
by A11, MESFUNC6:6;
then A13:
x in A /\ (great_eq_dom (f,a))
by A9, XBOOLE_0:def 4;
x in less_eq_dom (
f,
a)
by A11, A12, MESFUNC6:4;
hence
x in (A /\ (great_eq_dom (f,a))) /\ (less_eq_dom (f,a))
by A13, XBOOLE_0:def 4;
verum end;
then
A /\ (eq_dom (f,a)) c= (A /\ (great_eq_dom (f,a))) /\ (less_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; verum