let X be set ; for C being C_Measure of X
for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z)
let C be C_Measure of X; for W, Z being Subset of X holds C . (W \/ Z) <= (C . W) + (C . Z)
let W, Z be Subset of X; C . (W \/ Z) <= (C . W) + (C . Z)
reconsider P = {} as Subset of X by XBOOLE_1:2;
consider F being sequence of (bool X) such that
A1:
rng F = {W,Z,P}
and
A2:
F . 0 = W
and
A3:
F . 1 = Z
and
A4:
for n being Element of NAT st 1 < n holds
F . n = P
by MEASURE1:17;
A5:
(C * F) . 1 = C . Z
by A3, FUNCT_2:15;
set G = C * F;
A6:
union {W,Z,P} = W \/ Z
proof
thus
union {W,Z,P} c= W \/ Z
XBOOLE_0:def 10 W \/ Z c= union {W,Z,P}
let x be
object ;
TARSKI:def 3 ( not x in W \/ Z or x in union {W,Z,P} )
assume A7:
x in W \/ Z
;
x in union {W,Z,P}
hence
x in union {W,Z,P}
by TARSKI:def 4;
verum
end;
A10:
C is zeroed
by Def1;
A11:
for r being Element of NAT st 2 <= r holds
(C * F) . r = 0.
C is V92()
by Def1;
then A13:
C * F is V92()
by MEASURE1:25;
F . 2 = P
by A4;
then A14:
(C * F) . 2 = C . P
by FUNCT_2:15;
A15:
(C * F) . 0 = C . W
by A2, FUNCT_2:15;
consider y1, y2 being R_eal such that
A16:
y1 = (Ser (C * F)) . 1
and
A17:
y2 = (Ser (C * F)) . 0
;
(Ser (C * F)) . 2 =
y1 + ((C * F) . (1 + 1))
by A16, SUPINF_2:def 11
.=
((Ser (C * F)) . 1) + 0.
by A14, A16, A10, VALUED_0:def 19
.=
(Ser (C * F)) . 1
by XXREAL_3:4
.=
y2 + ((C * F) . (0 + 1))
by A17, SUPINF_2:def 11
.=
(C . W) + (C . Z)
by A5, A15, A17, SUPINF_2:def 11
;
then
SUM (C * F) = (C . W) + (C . Z)
by A13, A11, SUPINF_2:48;
hence
C . (W \/ Z) <= (C . W) + (C . Z)
by A1, A6, Def1; verum