set N = image_measure (F,M);

for s2 being Sep_Sequence of S2 holds SUM ((image_measure (F,M)) * s2) = (image_measure (F,M)) . (union (rng s2))

for s2 being Sep_Sequence of S2 holds SUM ((image_measure (F,M)) * s2) = (image_measure (F,M)) . (union (rng s2))

proof

hence
image_measure (F,M) is sigma-additive
by MEASURE1:def 6; :: thesis: verum
let s2 be Sep_Sequence of S2; :: thesis: SUM ((image_measure (F,M)) * s2) = (image_measure (F,M)) . (union (rng s2))

A1: for x, y being object st x <> y holds

((" F) * s2) . x misses ((" F) * s2) . y

then ex f being Function st

( s2 = f & dom f = NAT & rng f c= S2 ) by FUNCT_2:def 2;

then A8: ( dom s2 = NAT & rng s2 c= S2 ) ;

A9: dom (" F) = bool Omega2 by FUNCT_2:def 1;

then A10: dom ((" F) * s2) = NAT by A8, RELAT_1:27;

A11: for x being object st x in NAT holds

((" F) * s2) . x in S1

reconsider s1 = (" F) * s2 as Sep_Sequence of S1 by A1, PROB_2:def 2, A10, FUNCT_2:3, A11;

A15: SUM (M * s1) = M . (union (rng s1)) by MEASURE1:def 6;

for x being object holds

( x in union (rng ((" F) * s2)) iff x in F " (union (rng s2)) )

union (rng s2) is Element of S2 by MEASURE1:24;

hence SUM ((image_measure (F,M)) * s2) = (image_measure (F,M)) . (union (rng s2)) by A15, A24, A35, Def6; :: thesis: verum

end;A1: for x, y being object st x <> y holds

((" F) * s2) . x misses ((" F) * s2) . y

proof

s2 in Funcs (NAT,S2)
by FUNCT_2:8;
let x, y be object ; :: thesis: ( x <> y implies ((" F) * s2) . x misses ((" F) * s2) . y )

assume A2: x <> y ; :: thesis: ((" F) * s2) . x misses ((" F) * s2) . y

A3: (F " (s2 . x)) /\ (F " (s2 . y)) = F " ((s2 . x) /\ (s2 . y)) by FUNCT_1:68

.= F " {} by A2, XBOOLE_0:def 7, PROB_2:def 2

.= {} ;

end;assume A2: x <> y ; :: thesis: ((" F) * s2) . x misses ((" F) * s2) . y

A3: (F " (s2 . x)) /\ (F " (s2 . y)) = F " ((s2 . x) /\ (s2 . y)) by FUNCT_1:68

.= F " {} by A2, XBOOLE_0:def 7, PROB_2:def 2

.= {} ;

per cases
( ( x in dom ((" F) * s2) & y in dom ((" F) * s2) ) or not x in dom ((" F) * s2) or not y in dom ((" F) * s2) )
;

end;

suppose A4:
( x in dom ((" F) * s2) & y in dom ((" F) * s2) )
; :: thesis: ((" F) * s2) . x misses ((" F) * s2) . y

then A5:
( x in dom s2 & s2 . x in dom (" F) )
by FUNCT_1:11;

A6: ( y in dom s2 & s2 . y in dom (" F) ) by A4, FUNCT_1:11;

A7: ((" F) * s2) . x = (" F) . (s2 . x) by A4, FUNCT_1:12

.= F " (s2 . x) by MEASURE6:def 3, A5 ;

((" F) * s2) . y = (" F) . (s2 . y) by A4, FUNCT_1:12

.= F " (s2 . y) by A6, MEASURE6:def 3 ;

hence ((" F) * s2) . x misses ((" F) * s2) . y by A7, A3; :: thesis: verum

end;A6: ( y in dom s2 & s2 . y in dom (" F) ) by A4, FUNCT_1:11;

A7: ((" F) * s2) . x = (" F) . (s2 . x) by A4, FUNCT_1:12

.= F " (s2 . x) by MEASURE6:def 3, A5 ;

((" F) * s2) . y = (" F) . (s2 . y) by A4, FUNCT_1:12

.= F " (s2 . y) by A6, MEASURE6:def 3 ;

hence ((" F) * s2) . x misses ((" F) * s2) . y by A7, A3; :: thesis: verum

then ex f being Function st

( s2 = f & dom f = NAT & rng f c= S2 ) by FUNCT_2:def 2;

then A8: ( dom s2 = NAT & rng s2 c= S2 ) ;

A9: dom (" F) = bool Omega2 by FUNCT_2:def 1;

then A10: dom ((" F) * s2) = NAT by A8, RELAT_1:27;

A11: for x being object st x in NAT holds

((" F) * s2) . x in S1

proof

then A14:
(" F) * s2 is Function of NAT,S1
by A10, FUNCT_2:3;
let x be object ; :: thesis: ( x in NAT implies ((" F) * s2) . x in S1 )

assume x in NAT ; :: thesis: ((" F) * s2) . x in S1

then reconsider n = x as Element of NAT ;

end;assume x in NAT ; :: thesis: ((" F) * s2) . x in S1

then reconsider n = x as Element of NAT ;

per cases
( n in dom ((" F) * s2) or not n in dom ((" F) * s2) )
;

end;

reconsider s1 = (" F) * s2 as Sep_Sequence of S1 by A1, PROB_2:def 2, A10, FUNCT_2:3, A11;

A15: SUM (M * s1) = M . (union (rng s1)) by MEASURE1:def 6;

now :: thesis: for n being Element of NAT holds (M * s1) . n = ((image_measure (F,M)) * s2) . n

then A24:
M * s1 = (image_measure (F,M)) * s2
by FUNCT_2:def 8;let n be Element of NAT ; :: thesis: (M * s1) . b_{1} = ((image_measure (F,M)) * s2) . b_{1}

A16: (M * s1) . n = M . (s1 . n) by FUNCT_2:15;

A17: ((image_measure (F,M)) * s2) . n = (image_measure (F,M)) . (s2 . n) by FUNCT_2:15;

end;A16: (M * s1) . n = M . (s1 . n) by FUNCT_2:15;

A17: ((image_measure (F,M)) * s2) . n = (image_measure (F,M)) . (s2 . n) by FUNCT_2:15;

per cases
( n in dom ((" F) * s2) or not n in dom ((" F) * s2) )
;

end;

suppose A18:
n in dom ((" F) * s2)
; :: thesis: (M * s1) . b_{1} = ((image_measure (F,M)) * s2) . b_{1}

then A19:
( n in dom s2 & s2 . n in dom (" F) )
by FUNCT_1:11;

A20: s1 . n = (" F) . (s2 . n) by A18, FUNCT_1:12

.= F " (s2 . n) by A19, MEASURE6:def 3 ;

thus (M * s1) . n = M . (F " (s2 . n)) by A20, FUNCT_2:15

.= (image_measure (F,M)) . (s2 . n) by Def6

.= ((image_measure (F,M)) * s2) . n by FUNCT_2:15 ; :: thesis: verum

end;A20: s1 . n = (" F) . (s2 . n) by A18, FUNCT_1:12

.= F " (s2 . n) by A19, MEASURE6:def 3 ;

thus (M * s1) . n = M . (F " (s2 . n)) by A20, FUNCT_2:15

.= (image_measure (F,M)) . (s2 . n) by Def6

.= ((image_measure (F,M)) * s2) . n by FUNCT_2:15 ; :: thesis: verum

suppose A21:
not n in dom ((" F) * s2)
; :: thesis: (M * s1) . b_{1} = ((image_measure (F,M)) * s2) . b_{1}

A22: (M * s1) . n =
M . {}
by A21, A16, FUNCT_1:def 2

.= 0 by VALUED_0:def 19 ;

A23: ( not n in dom s2 or not s2 . n in dom (" F) ) by A21, FUNCT_1:11;

s2 . n in S2 ;

then s2 . n = {} by FUNCT_1:def 2, A23, A9;

hence (M * s1) . n = ((image_measure (F,M)) * s2) . n by A22, A17, VALUED_0:def 19; :: thesis: verum

end;.= 0 by VALUED_0:def 19 ;

A23: ( not n in dom s2 or not s2 . n in dom (" F) ) by A21, FUNCT_1:11;

s2 . n in S2 ;

then s2 . n = {} by FUNCT_1:def 2, A23, A9;

hence (M * s1) . n = ((image_measure (F,M)) * s2) . n by A22, A17, VALUED_0:def 19; :: thesis: verum

for x being object holds

( x in union (rng ((" F) * s2)) iff x in F " (union (rng s2)) )

proof

then A35:
union (rng ((" F) * s2)) = F " (union (rng s2))
by TARSKI:2;
let x be object ; :: thesis: ( x in union (rng ((" F) * s2)) iff x in F " (union (rng s2)) )

then A29: ( x in dom F & F . x in union (rng s2) ) by FUNCT_1:def 7;

then consider Z being set such that

A30: ( F . x in Z & Z in rng s2 ) by TARSKI:def 4;

consider n being Element of NAT such that

A31: Z = s2 . n by A30, FUNCT_2:113;

A32: x in F " Z by A30, FUNCT_1:def 7, A29;

A33: ( n in dom s2 & s2 . n in dom (" F) ) by FUNCT_1:11, A10;

A34: ((" F) * s2) . n = (" F) . (s2 . n) by A10, FUNCT_1:12

.= F " (s2 . n) by A33, MEASURE6:def 3 ;

F " Z in rng ((" F) * s2) by A31, A10, A34, FUNCT_1:3;

hence x in union (rng ((" F) * s2)) by A32, TARSKI:def 4; :: thesis: verum

end;hereby :: thesis: ( x in F " (union (rng s2)) implies x in union (rng ((" F) * s2)) )

assume
x in F " (union (rng s2))
; :: thesis: x in union (rng ((" F) * s2))assume
x in union (rng ((" F) * s2))
; :: thesis: x in F " (union (rng s2))

then consider Y being set such that

A25: ( x in Y & Y in rng ((" F) * s2) ) by TARSKI:def 4;

consider n being Element of NAT such that

A26: Y = ((" F) * s2) . n by A25, A14, FUNCT_2:113;

A27: ( n in dom s2 & s2 . n in dom (" F) ) by FUNCT_1:11, A10;

A28: ((" F) * s2) . n = (" F) . (s2 . n) by A10, FUNCT_1:12

.= F " (s2 . n) by A27, MEASURE6:def 3 ;

s2 . n c= union (rng s2) by ZFMISC_1:74, FUNCT_2:4;

then F " (s2 . n) c= F " (union (rng s2)) by RELAT_1:143;

hence x in F " (union (rng s2)) by A25, A26, A28; :: thesis: verum

end;then consider Y being set such that

A25: ( x in Y & Y in rng ((" F) * s2) ) by TARSKI:def 4;

consider n being Element of NAT such that

A26: Y = ((" F) * s2) . n by A25, A14, FUNCT_2:113;

A27: ( n in dom s2 & s2 . n in dom (" F) ) by FUNCT_1:11, A10;

A28: ((" F) * s2) . n = (" F) . (s2 . n) by A10, FUNCT_1:12

.= F " (s2 . n) by A27, MEASURE6:def 3 ;

s2 . n c= union (rng s2) by ZFMISC_1:74, FUNCT_2:4;

then F " (s2 . n) c= F " (union (rng s2)) by RELAT_1:143;

hence x in F " (union (rng s2)) by A25, A26, A28; :: thesis: verum

then A29: ( x in dom F & F . x in union (rng s2) ) by FUNCT_1:def 7;

then consider Z being set such that

A30: ( F . x in Z & Z in rng s2 ) by TARSKI:def 4;

consider n being Element of NAT such that

A31: Z = s2 . n by A30, FUNCT_2:113;

A32: x in F " Z by A30, FUNCT_1:def 7, A29;

A33: ( n in dom s2 & s2 . n in dom (" F) ) by FUNCT_1:11, A10;

A34: ((" F) * s2) . n = (" F) . (s2 . n) by A10, FUNCT_1:12

.= F " (s2 . n) by A33, MEASURE6:def 3 ;

F " Z in rng ((" F) * s2) by A31, A10, A34, FUNCT_1:3;

hence x in union (rng ((" F) * s2)) by A32, TARSKI:def 4; :: thesis: verum

union (rng s2) is Element of S2 by MEASURE1:24;

hence SUM ((image_measure (F,M)) * s2) = (image_measure (F,M)) . (union (rng s2)) by A15, A24, A35, Def6; :: thesis: verum