let X be set ; :: thesis: for S being SigmaField of X

for a, b being R_eal ex M being Function of S,ExtREAL st

for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

let S be SigmaField of X; :: thesis: for a, b being R_eal ex M being Function of S,ExtREAL st

for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

let a, b be R_eal; :: thesis: ex M being Function of S,ExtREAL st

for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

defpred S_{1}[ object , object ] means ( ( $1 = {} implies $2 = a ) & ( $1 <> {} implies $2 = b ) );

A1: for x being object st x in S holds

ex y being object st

( y in ExtREAL & S_{1}[x,y] )

for x being object st x in S holds

S_{1}[x,F . x]
from FUNCT_2:sch 1(A1);

then consider M being Function of S,ExtREAL such that

A2: for x being object st x in S holds

S_{1}[x,M . x]
;

take M ; :: thesis: for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

thus for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) ) by A2; :: thesis: verum

for a, b being R_eal ex M being Function of S,ExtREAL st

for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

let S be SigmaField of X; :: thesis: for a, b being R_eal ex M being Function of S,ExtREAL st

for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

let a, b be R_eal; :: thesis: ex M being Function of S,ExtREAL st

for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

defpred S

A1: for x being object st x in S holds

ex y being object st

( y in ExtREAL & S

proof

ex F being Function of S,ExtREAL st
let x be object ; :: thesis: ( x in S implies ex y being object st

( y in ExtREAL & S_{1}[x,y] ) )

( x <> {} implies ex y being set st

( y in ExtREAL & S_{1}[x,y] ) )
;

hence ( x in S implies ex y being object st

( y in ExtREAL & S_{1}[x,y] ) )
; :: thesis: verum

end;( y in ExtREAL & S

( x <> {} implies ex y being set st

( y in ExtREAL & S

hence ( x in S implies ex y being object st

( y in ExtREAL & S

for x being object st x in S holds

S

then consider M being Function of S,ExtREAL such that

A2: for x being object st x in S holds

S

take M ; :: thesis: for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) )

thus for A being Element of S holds

( ( A = {} implies M . A = a ) & ( A <> {} implies M . A = b ) ) by A2; :: thesis: verum