reconsider M = S --> 0. as Function of S,ExtREAL ;

A1: for A, B being Element of S st A misses B holds

M . (A \/ B) = (M . A) + (M . B)

( ( for x being Element of S holds 0. <= M . x ) & M . {} = 0. ) by FUNCOP_1:7, PROB_1:4;

hence ( M is V94() & M is additive & M is zeroed ) by A1, VALUED_0:def 19; :: thesis: verum

A1: for A, B being Element of S st A misses B holds

M . (A \/ B) = (M . A) + (M . B)

proof

take
M
; :: thesis: ( M is V94() & M is additive & M is zeroed )
let A, B be Element of S; :: thesis: ( A misses B implies M . (A \/ B) = (M . A) + (M . B) )

assume A misses B ; :: thesis: M . (A \/ B) = (M . A) + (M . B)

A2: ( M . A = 0. & M . B = 0. ) by FUNCOP_1:7;

reconsider A = A, B = B as set ;

reconsider A = A, B = B as Element of S ;

0. = (M . A) + (M . B) by A2, XXREAL_3:4;

hence M . (A \/ B) = (M . A) + (M . B) by FUNCOP_1:7; :: thesis: verum

end;assume A misses B ; :: thesis: M . (A \/ B) = (M . A) + (M . B)

A2: ( M . A = 0. & M . B = 0. ) by FUNCOP_1:7;

reconsider A = A, B = B as set ;

reconsider A = A, B = B as Element of S ;

0. = (M . A) + (M . B) by A2, XXREAL_3:4;

hence M . (A \/ B) = (M . A) + (M . B) by FUNCOP_1:7; :: thesis: verum

( ( for x being Element of S holds 0. <= M . x ) & M . {} = 0. ) by FUNCOP_1:7, PROB_1:4;

hence ( M is V94() & M is additive & M is zeroed ) by A1, VALUED_0:def 19; :: thesis: verum