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₁[ 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₁[x,y] )

proof

let x be object ; :: thesis: ( x in S implies ex y being object st
( y in ExtREAL & S₁[x,y] ) )
( x <> {} implies ex y being set st
( y in ExtREAL & S₁[x,y] ) ) ;
hence ( x in S implies ex y being object st
( y in ExtREAL & S₁[x,y] ) ) ; :: thesis: verum

end;

ex F being Function of S,ExtREAL st
for x being object st x in S holds
S₁[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₁[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