let X be set ; :: thesis: for P being non empty Subset-Family of X holds
( P --> 0. is nonnegative & P --> 0. is additive & P --> 0. is zeroed )
let P be non empty Subset-Family of X; :: thesis: ( P --> 0. is nonnegative & P --> 0. is additive & P --> 0. is zeroed )
set M = P --> 0.;
for A being Element of P holds 0. <= (P --> 0.) . A ;
hence P --> 0. is nonnegative by MEASURE1:def 2; :: thesis: ( P --> 0. is additive & P --> 0. is zeroed )

now :: thesis: for A, B being Element of P st A misses B & A \/ B in P holds
(P --> 0.) . (A \/ B) = ((P --> 0.) . A) + ((P --> 0.) . B)

let A, B be Element of P; :: thesis: ( A misses B & A \/ B in P implies (P --> 0.) . (A \/ B) = ((P --> 0.) . A) + ((P --> 0.) . B) )
assume ( A misses B & A \/ B in P ) ; :: thesis: (P --> 0.) . (A \/ B) = ((P --> 0.) . A) + ((P --> 0.) . B)
then reconsider D = A \/ B as Element of P ;
( (P --> 0.) . A = 0. & (P --> 0.) . B = 0. & (P --> 0.) . D = 0. ) by FUNCOP_1:7;
hence (P --> 0.) . (A \/ B) = ((P --> 0.) . A) + ((P --> 0.) . B) ; :: thesis: verum

end;

hence P --> 0. is additive by MEASURE1:def 3; :: thesis: P --> 0. is zeroed

per cases ( {} in P or not {} in P ) ;

suppose {} in P ; :: thesis: P --> 0. is zeroed

then (P --> 0.) . {} = 0. by FUNCOP_1:7;
hence P --> 0. is zeroed by VALUED_0:def 19; :: thesis: verum

end;

suppose not {} in P ; :: thesis: P --> 0. is zeroed

then not {} in dom (P --> 0.) ;
then (P --> 0.) . {} = 0 by FUNCT_1:def 2;
hence P --> 0. is zeroed by VALUED_0:def 19; :: thesis: verum

end;

end;