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)
proof
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;
take M ; :: thesis: ( M is V94() & M is additive & M is zeroed )
( ( 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