ex D being Function of (sigma_Field C),ExtREAL st
for A being Subset of X st A in sigma_Field C holds
D . A = C . A

proof

deffunc H₁( object ) -> set = C . $1;
A1: for S being object st S in sigma_Field C holds
H₁(S) in ExtREAL

proof

let S be object ; :: thesis: ( S in sigma_Field C implies H₁(S) in ExtREAL )
assume S in sigma_Field C ; :: thesis: H₁(S) in ExtREAL
reconsider S = S as set by TARSKI:1;
C . S in ExtREAL ;
hence H₁(S) in ExtREAL ; :: thesis: verum

end;

consider D being Function of (sigma_Field C),ExtREAL such that
A2: for S being object st S in sigma_Field C holds
D . S = H₁(S) from FUNCT_2:sch 2(A1);
take D ; :: thesis: for A being Subset of X st A in sigma_Field C holds
D . A = C . A
thus for A being Subset of X st A in sigma_Field C holds
D . A = C . A by A2; :: thesis: verum

end;

then consider D being Function of (sigma_Field C),ExtREAL such that
A3: for A being Subset of X st A in sigma_Field C holds
D . A = C . A ;
take D ; :: thesis: for A being Subset of X st A in sigma_Field C holds
D . A = C . A
thus for A being Subset of X st A in sigma_Field C holds
D . A = C . A by A3; :: thesis: verum