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₁( set ) -> Element of ExtREAL = C . $1;
A1: for S being set st S in sigma_Field C holds
H₁(S) in ExtREAL ;
consider D being Function of (sigma_Field C),ExtREAL such that
A2: for S being set 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