let X be non empty set ; :: thesis: for S being SigmaField of X
for A being Element of S
for p being R_eal holds X --> p is A -measurable
let S be SigmaField of X; :: thesis: for A being Element of S
for p being R_eal holds X --> p is A -measurable
let A be Element of S; :: thesis: for p being R_eal holds X --> p is A -measurable
let p be R_eal; :: thesis: X --> p is A -measurable
A0: dom (X --> p) = X by FUNCOP_1:13;
for r being Real holds A /\ (great_eq_dom ((X --> p),r)) in S

proof

let r be Real; :: thesis: A /\ (great_eq_dom ((X --> p),r)) in S

per cases ( r > p or r <= p ) ;

suppose A2: r > p ; :: thesis: A /\ (great_eq_dom ((X --> p),r)) in S

for x being object holds not x in great_eq_dom ((X --> p),r)

proof

let x be object ; :: thesis: not x in great_eq_dom ((X --> p),r)

hereby :: thesis: verum

assume x in great_eq_dom ((X --> p),r) ; :: thesis: contradiction
then ( x in dom (X --> p) & r <= (X --> p) . x ) by MESFUNC1:def 14;
hence contradiction by A2, FUNCOP_1:7; :: thesis: verum

end;

end;

then great_eq_dom ((X --> p),r) = {} by XBOOLE_0:def 1;
hence A /\ (great_eq_dom ((X --> p),r)) in S by MEASURE1:7; :: thesis: verum

end;

suppose A4: r <= p ; :: thesis: A /\ (great_eq_dom ((X --> p),r)) in S

now :: thesis: for x being object st x in X holds
x in great_eq_dom ((X --> p),r)

let x be object ; :: thesis: ( x in X implies x in great_eq_dom ((X --> p),r) )
assume A6: x in X ; :: thesis: x in great_eq_dom ((X --> p),r)
then (X --> p) . x = p by FUNCOP_1:7;
hence x in great_eq_dom ((X --> p),r) by A0, A4, A6, MESFUNC1:def 14; :: thesis: verum

end;

then X c= great_eq_dom ((X --> p),r) ;
then great_eq_dom ((X --> p),r) = X ;
then A /\ (great_eq_dom ((X --> p),r)) = A by XBOOLE_1:28;
hence A /\ (great_eq_dom ((X --> p),r)) in S ; :: thesis: verum

end;

end;

end;

hence X --> p is A -measurable by A0, MESFUNC1:27; :: thesis: verum