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

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

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

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:
thus for A being Subset of X st A in sigma_Field C holds
D . A = C . A by A2; :: thesis:

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:
thus for A being Subset of X st A in sigma_Field C holds
D . A = C . A by A3; :: thesis: