let D1, D2 be Function of (sigma_Field C),ExtREAL; :: thesis: ( ( for A being Subset of X st A in sigma_Field C holds
D1 . A = C . A ) & ( for A being Subset of X st A in sigma_Field C holds
D2 . A = C . A ) implies D1 = D2 )
assume that
A4: for A being Subset of X st A in sigma_Field C holds
D1 . A = C . A and
A5: for A being Subset of X st A in sigma_Field C holds
D2 . A = C . A ; :: thesis: D1 = D2
A6: for A being object st A in sigma_Field C holds
D1 . A = D2 . A

proof

let A be object ; :: thesis: ( A in sigma_Field C implies D1 . A = D2 . A )
assume A7: A in sigma_Field C ; :: thesis: D1 . A = D2 . A
then reconsider A = A as Subset of X ;
D1 . A = C . A by A4, A7
.= D2 . A by A5, A7 ;
hence D1 . A = D2 . A ; :: thesis: verum

end;

A8: sigma_Field C = dom D2 by FUNCT_2:def 1;
sigma_Field C = dom D1 by FUNCT_2:def 1;
hence D1 = D2 by A8, A6, FUNCT_1:2; :: thesis: verum