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))

proof

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

proof

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
.= {} ;

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) ) ;

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;

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

then ( ((" F) * s2) . x = {} or ((" F) * s2) . y = {} ) by FUNCT_1:def 2;
hence ((" F) * s2) . x misses ((" F) * s2) . y ; :: thesis: verum

end;

end;

end;

s2 in Funcs (NAT,S2) by FUNCT_2:8;
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

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 ;

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

suppose A12: n in dom ((" F) * s2) ; :: thesis: ((" F) * s2) . x in S1

then A13: ( n in dom s2 & s2 . n in dom (" F) ) by FUNCT_1:11;
((" F) * s2) . n = (" F) . (s2 . n) by A12, FUNCT_1:12
.= F " (s2 . n) by A13, MEASURE6:def 3 ;
hence ((" F) * s2) . x in S1 by FINANCE1:def 5; :: thesis: verum

end;

suppose not n in dom ((" F) * s2) ; :: thesis: ((" F) * s2) . x in S1

then ((" F) * s2) . n = {} by FUNCT_1:def 2;
hence ((" F) * s2) . x in S1 by PROB_1:4; :: thesis: verum

end;

end;

end;

then A14: (" F) * s2 is Function of NAT,S1 by A10, FUNCT_2:3;
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

let n be Element of NAT ; :: thesis: (M * s1) . b₁ = ((image_measure (F,M)) * s2) . b₁
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) ) ;

suppose A18: n in dom ((" F) * s2) ; :: thesis: (M * s1) . b₁ = ((image_measure (F,M)) * s2) . b₁

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;

suppose A21: not n in dom ((" F) * s2) ; :: thesis: (M * s1) . b₁ = ((image_measure (F,M)) * s2) . b₁

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;

end;

end;

then A24: M * s1 = (image_measure (F,M)) * s2 by FUNCT_2:def 8;
for x being object holds
( x in union (rng ((" F) * s2)) iff x in F " (union (rng s2)) )

proof

let x be object ; :: thesis: ( x in union (rng ((" F) * s2)) iff x in F " (union (rng s2)) )

hereby :: thesis: ( x in F " (union (rng s2)) implies 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;

assume x in F " (union (rng s2)) ; :: thesis: x in union (rng ((" F) * 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;

then A35: union (rng ((" F) * s2)) = F " (union (rng s2)) by TARSKI:2;
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;

hence image_measure (F,M) is sigma-additive by MEASURE1:def 6; :: thesis: verum