let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & g is_simple_func_in S implies f + g is_simple_func_in S )

assume that

A1: f is_simple_func_in S and

A4: g is_simple_func_in S ; :: thesis: f + g is_simple_func_in S

g is V70() by A4, MESFUNC2:def 4;

then A8: dom (f + g) = (dom f) /\ (dom g) by MESFUNC2:2;

consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that

A10: F,a are_Re-presentation_of f by A1, MESFUNC3:12;

consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that

A9: G,b are_Re-presentation_of g by A4, MESFUNC3:12;

set la = len a;

set lb = len b;

A11: ( dom F = dom a & dom G = dom b ) by A9, A10, MESFUNC3:def 1;

deffunc H_{1}( Nat) -> M8(X,S) = (F . ((($1 -' 1) div (len b)) + 1)) /\ (G . ((($1 -' 1) mod (len b)) + 1));

consider FG being FinSequence such that

A12: len FG = (len a) * (len b) and

A13: for k being Nat st k in dom FG holds

FG . k = H_{1}(k)
from FINSEQ_1:sch 2();

A14: dom FG = Seg ((len a) * (len b)) by A12, FINSEQ_1:def 3;

for k, l being Nat st k in dom FG & l in dom FG & k <> l holds

FG . k misses FG . l

A51: dom f = union (rng F) by A10, MESFUNC3:def 1;

A70: dom g = union (rng G) by A9, MESFUNC3:def 1;

A71: dom (f + g) = union (rng FG)

for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds

(f + g) . x = (f + g) . y

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_simple_func_in S & g is_simple_func_in S holds

f + g is_simple_func_in S

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & g is_simple_func_in S implies f + g is_simple_func_in S )

assume that

A1: f is_simple_func_in S and

A4: g is_simple_func_in S ; :: thesis: f + g is_simple_func_in S

g is V70() by A4, MESFUNC2:def 4;

then A8: dom (f + g) = (dom f) /\ (dom g) by MESFUNC2:2;

consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that

A10: F,a are_Re-presentation_of f by A1, MESFUNC3:12;

consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that

A9: G,b are_Re-presentation_of g by A4, MESFUNC3:12;

set la = len a;

set lb = len b;

A11: ( dom F = dom a & dom G = dom b ) by A9, A10, MESFUNC3:def 1;

deffunc H

consider FG being FinSequence such that

A12: len FG = (len a) * (len b) and

A13: for k being Nat st k in dom FG holds

FG . k = H

A14: dom FG = Seg ((len a) * (len b)) by A12, FINSEQ_1:def 3;

now :: thesis: for k being Nat st k in dom FG holds

FG . k in S

then reconsider FG = FG as FinSequence of S by FINSEQ_2:12;FG . k in S

let k be Nat; :: thesis: ( k in dom FG implies FG . k in S )

assume k in dom FG ; :: thesis: FG . k in S

then FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13;

hence FG . k in S ; :: thesis: verum

end;assume k in dom FG ; :: thesis: FG . k in S

then FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13;

hence FG . k in S ; :: thesis: verum

for k, l being Nat st k in dom FG & l in dom FG & k <> l holds

FG . k misses FG . l

proof

then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
let k, l be Nat; :: thesis: ( k in dom FG & l in dom FG & k <> l implies FG . k misses FG . l )

assume that

A25: k in dom FG and

A26: l in dom FG and

A27: k <> l ; :: thesis: FG . k misses FG . l

set m = ((l -' 1) mod (len b)) + 1;

set n = ((l -' 1) div (len b)) + 1;

set j = ((k -' 1) mod (len b)) + 1;

set i = ((k -' 1) div (len b)) + 1;

A29: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A25;

A30: k in Seg ((len a) * (len b)) by A12, A25, FINSEQ_1:def 3;

A31: ( 1 <= k & k <= (len a) * (len b) & 1 <= l & l <= (len a) * (len b) ) by A12, A25, A26, FINSEQ_3:25;

then A33: ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by NAT_D:def 3, XXREAL_0:2;

A34: len b <> 0 by A30;

then len b >= 1 by NAT_1:14;

then A35: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A33, NAT_2:15;

k -' 1 <= ((len a) * (len b)) -' 1 by A31, NAT_D:42;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A35, NAT_2:24;

then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then ((k -' 1) div (len b)) + 1 <= len a by A34, NAT_D:18;

then A37: ((k -' 1) div (len b)) + 1 in dom F by A11, NAT_1:11, FINSEQ_3:25;

( ((l -' 1) mod (len b)) + 1 <= len b & ((k -' 1) mod (len b)) + 1 <= len b ) by A34, NAT_D:1, NAT_1:13;

then A42: ( ((l -' 1) mod (len b)) + 1 in dom G & ((k -' 1) mod (len b)) + 1 in dom G ) by A11, NAT_1:11, FINSEQ_3:25;

l -' 1 <= ((len a) * (len b)) -' 1 by A31, NAT_D:42;

then (l -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A35, NAT_2:24;

then ((l -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then ((l -' 1) div (len b)) + 1 <= len a by A34, NAT_D:18;

then A44: ((l -' 1) div (len b)) + 1 in dom F by A11, NAT_1:11, FINSEQ_3:25;

(l -' 1) + 1 = ((((((l -' 1) div (len b)) + 1) - 1) * (len b)) + ((((l -' 1) mod (len b)) + 1) - 1)) + 1 by A34, NAT_D:2;

then A40: (l - 1) + 1 = (((((l -' 1) div (len b)) + 1) - 1) * (len b)) + (((l -' 1) mod (len b)) + 1) by A31, XREAL_1:233;

(k -' 1) + 1 = ((((((k -' 1) div (len b)) + 1) - 1) * (len b)) + ((((k -' 1) mod (len b)) + 1) - 1)) + 1 by A34, NAT_D:2;

then A41: (k - 1) + 1 = (((((k -' 1) div (len b)) + 1) - 1) * (len b)) + (((k -' 1) mod (len b)) + 1) by A31, XREAL_1:233;

end;assume that

A25: k in dom FG and

A26: l in dom FG and

A27: k <> l ; :: thesis: FG . k misses FG . l

set m = ((l -' 1) mod (len b)) + 1;

set n = ((l -' 1) div (len b)) + 1;

set j = ((k -' 1) mod (len b)) + 1;

set i = ((k -' 1) div (len b)) + 1;

A29: FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A25;

A30: k in Seg ((len a) * (len b)) by A12, A25, FINSEQ_1:def 3;

A31: ( 1 <= k & k <= (len a) * (len b) & 1 <= l & l <= (len a) * (len b) ) by A12, A25, A26, FINSEQ_3:25;

then A33: ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by NAT_D:def 3, XXREAL_0:2;

A34: len b <> 0 by A30;

then len b >= 1 by NAT_1:14;

then A35: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A33, NAT_2:15;

k -' 1 <= ((len a) * (len b)) -' 1 by A31, NAT_D:42;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A35, NAT_2:24;

then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then ((k -' 1) div (len b)) + 1 <= len a by A34, NAT_D:18;

then A37: ((k -' 1) div (len b)) + 1 in dom F by A11, NAT_1:11, FINSEQ_3:25;

( ((l -' 1) mod (len b)) + 1 <= len b & ((k -' 1) mod (len b)) + 1 <= len b ) by A34, NAT_D:1, NAT_1:13;

then A42: ( ((l -' 1) mod (len b)) + 1 in dom G & ((k -' 1) mod (len b)) + 1 in dom G ) by A11, NAT_1:11, FINSEQ_3:25;

l -' 1 <= ((len a) * (len b)) -' 1 by A31, NAT_D:42;

then (l -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A35, NAT_2:24;

then ((l -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then ((l -' 1) div (len b)) + 1 <= len a by A34, NAT_D:18;

then A44: ((l -' 1) div (len b)) + 1 in dom F by A11, NAT_1:11, FINSEQ_3:25;

(l -' 1) + 1 = ((((((l -' 1) div (len b)) + 1) - 1) * (len b)) + ((((l -' 1) mod (len b)) + 1) - 1)) + 1 by A34, NAT_D:2;

then A40: (l - 1) + 1 = (((((l -' 1) div (len b)) + 1) - 1) * (len b)) + (((l -' 1) mod (len b)) + 1) by A31, XREAL_1:233;

(k -' 1) + 1 = ((((((k -' 1) div (len b)) + 1) - 1) * (len b)) + ((((k -' 1) mod (len b)) + 1) - 1)) + 1 by A34, NAT_D:2;

then A41: (k - 1) + 1 = (((((k -' 1) div (len b)) + 1) - 1) * (len b)) + (((k -' 1) mod (len b)) + 1) by A31, XREAL_1:233;

per cases
( ((k -' 1) div (len b)) + 1 <> ((l -' 1) div (len b)) + 1 or ((k -' 1) mod (len b)) + 1 <> ((l -' 1) mod (len b)) + 1 )
by A27, A40, A41;

end;

suppose
((k -' 1) div (len b)) + 1 <> ((l -' 1) div (len b)) + 1
; :: thesis: FG . k misses FG . l

then A45:
F . (((k -' 1) div (len b)) + 1) misses F . (((l -' 1) div (len b)) + 1)
by A37, A44, MESFUNC3:4;

(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A13, A26, A29

.= (F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16

.= (F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16

.= ((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by XBOOLE_1:16

.= {} by A45 ;

hence FG . k misses FG . l ; :: thesis: verum

end;(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A13, A26, A29

.= (F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16

.= (F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16

.= ((F . (((k -' 1) div (len b)) + 1)) /\ (F . (((l -' 1) div (len b)) + 1))) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by XBOOLE_1:16

.= {} by A45 ;

hence FG . k misses FG . l ; :: thesis: verum

suppose
((k -' 1) mod (len b)) + 1 <> ((l -' 1) mod (len b)) + 1
; :: thesis: FG . k misses FG . l

then A46:
G . (((k -' 1) mod (len b)) + 1) misses G . (((l -' 1) mod (len b)) + 1)
by A42, MESFUNC3:4;

(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A13, A26, A29

.= (F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16

.= (F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16

.= {} by A46 ;

hence FG . k misses FG . l ; :: thesis: verum

end;(FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1))) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1))) by A13, A26, A29

.= (F . (((k -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16

.= (F . (((k -' 1) div (len b)) + 1)) /\ ((F . (((l -' 1) div (len b)) + 1)) /\ ((G . (((k -' 1) mod (len b)) + 1)) /\ (G . (((l -' 1) mod (len b)) + 1)))) by XBOOLE_1:16

.= {} by A46 ;

hence FG . k misses FG . l ; :: thesis: verum

A51: dom f = union (rng F) by A10, MESFUNC3:def 1;

A70: dom g = union (rng G) by A9, MESFUNC3:def 1;

A71: dom (f + g) = union (rng FG)

proof

A107:
for k being Nat
thus
dom (f + g) c= union (rng FG)
:: according to XBOOLE_0:def 10 :: thesis: union (rng FG) c= dom (f + g)

assume z in union (rng FG) ; :: thesis: z in dom (f + g)

then consider Y being set such that

A96: z in Y and

A97: Y in rng FG by TARSKI:def 4;

consider k being object such that

A98: k in dom FG and

A99: Y = FG . k by A97, FUNCT_1:def 3;

reconsider k = k as Element of NAT by A98;

set j = ((k -' 1) mod (len b)) + 1;

set i = ((k -' 1) div (len b)) + 1;

FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A98;

then A100: ( z in F . (((k -' 1) div (len b)) + 1) & z in G . (((k -' 1) mod (len b)) + 1) ) by A96, A99, XBOOLE_0:def 4;

A102: ( 1 <= k & k <= (len a) * (len b) ) by A12, A98, FINSEQ_3:25;

A103: len b <> 0 by A102;

then A104: len b >= 1 by NAT_1:14;

( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by A102, NAT_D:def 3, XXREAL_0:2;

then A105: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A104, NAT_2:15;

A106: ((len a) * (len b)) div (len b) = len a by A103, NAT_D:18;

k -' 1 <= ((len a) * (len b)) -' 1 by A102, NAT_D:42;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A105, NAT_2:24;

then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then ((k -' 1) div (len b)) + 1 in dom F by A11, A106, NAT_1:11, FINSEQ_3:25;

then F . (((k -' 1) div (len b)) + 1) in rng F by FUNCT_1:def 3;

then a107: z in dom f by A51, A100, TARSKI:def 4;

( 1 <= ((k -' 1) mod (len b)) + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by A103, NAT_D:1, NAT_1:11, NAT_1:13;

then ((k -' 1) mod (len b)) + 1 in dom G by A11, FINSEQ_3:25;

then G . (((k -' 1) mod (len b)) + 1) in rng G by FUNCT_1:def 3;

then z in dom g by A70, A100, TARSKI:def 4;

hence z in dom (f + g) by A8, a107, XBOOLE_0:def 4; :: thesis: verum

end;proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in union (rng FG) or z in dom (f + g) )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom (f + g) or z in union (rng FG) )

assume z in dom (f + g) ; :: thesis: z in union (rng FG)

then A72: ( z in dom f & z in dom g ) by A8, XBOOLE_0:def 4;

then consider Y being set such that

A73: z in Y and

A74: Y in rng F by A51, TARSKI:def 4;

consider Z being set such that

A75: z in Z and

A76: Z in rng G by A70, A72, TARSKI:def 4;

consider j being object such that

A77: j in dom G and

A78: Z = G . j by A76, FUNCT_1:def 3;

reconsider j = j as Element of NAT by A77;

consider j9 being Nat such that

A81: j = 1 + j9 by A77, Lm2, FINSEQ_3:25;

consider i being object such that

A82: i in dom F and

A83: Y = F . i by A74, FUNCT_1:def 3;

reconsider i = i as Element of NAT by A82;

consider i9 being Nat such that

A85: i = 1 + i9 by A82, Lm2, FINSEQ_3:25;

A80: ( 1 <= j & j <= len b ) by A11, A77, FINSEQ_3:25;

then A87: j9 < len b by A81, NAT_1:13;

reconsider k = ((i - 1) * (len b)) + j as Nat by A85;

A88: k >= 0 + j by A85, XREAL_1:6;

then A89: k -' 1 = k - 1 by A80, XREAL_1:233, XXREAL_0:2

.= (i9 * (len b)) + j9 by A85, A81 ;

then A90: i = ((k -' 1) div (len b)) + 1 by A85, A87, NAT_D:def 1;

i <= len a by A11, A82, FINSEQ_3:25;

then i - 1 <= (len a) - 1 by XREAL_1:9;

then (i - 1) * (len b) <= ((len a) - 1) * (len b) by XREAL_1:64;

then A91: k <= (((len a) - 1) * (len b)) + j by XREAL_1:6;

(((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by A80, XREAL_1:6;

then A92: k <= (len a) * (len b) by A91, XXREAL_0:2;

B1: k >= 1 by A80, A88, XXREAL_0:2;

then A93: k in Seg ((len a) * (len b)) by A92;

k in dom FG by A12, B1, A92, FINSEQ_3:25;

then A94: FG . k in rng FG by FUNCT_1:def 3;

A95: j = ((k -' 1) mod (len b)) + 1 by A81, A89, A87, NAT_D:def 2;

z in (F . i) /\ (G . j) by A73, A83, A75, A78, XBOOLE_0:def 4;

then z in FG . k by A13, A14, A90, A95, A93;

hence z in union (rng FG) by A94, TARSKI:def 4; :: thesis: verum

end;assume z in dom (f + g) ; :: thesis: z in union (rng FG)

then A72: ( z in dom f & z in dom g ) by A8, XBOOLE_0:def 4;

then consider Y being set such that

A73: z in Y and

A74: Y in rng F by A51, TARSKI:def 4;

consider Z being set such that

A75: z in Z and

A76: Z in rng G by A70, A72, TARSKI:def 4;

consider j being object such that

A77: j in dom G and

A78: Z = G . j by A76, FUNCT_1:def 3;

reconsider j = j as Element of NAT by A77;

consider j9 being Nat such that

A81: j = 1 + j9 by A77, Lm2, FINSEQ_3:25;

consider i being object such that

A82: i in dom F and

A83: Y = F . i by A74, FUNCT_1:def 3;

reconsider i = i as Element of NAT by A82;

consider i9 being Nat such that

A85: i = 1 + i9 by A82, Lm2, FINSEQ_3:25;

A80: ( 1 <= j & j <= len b ) by A11, A77, FINSEQ_3:25;

then A87: j9 < len b by A81, NAT_1:13;

reconsider k = ((i - 1) * (len b)) + j as Nat by A85;

A88: k >= 0 + j by A85, XREAL_1:6;

then A89: k -' 1 = k - 1 by A80, XREAL_1:233, XXREAL_0:2

.= (i9 * (len b)) + j9 by A85, A81 ;

then A90: i = ((k -' 1) div (len b)) + 1 by A85, A87, NAT_D:def 1;

i <= len a by A11, A82, FINSEQ_3:25;

then i - 1 <= (len a) - 1 by XREAL_1:9;

then (i - 1) * (len b) <= ((len a) - 1) * (len b) by XREAL_1:64;

then A91: k <= (((len a) - 1) * (len b)) + j by XREAL_1:6;

(((len a) - 1) * (len b)) + j <= (((len a) - 1) * (len b)) + (len b) by A80, XREAL_1:6;

then A92: k <= (len a) * (len b) by A91, XXREAL_0:2;

B1: k >= 1 by A80, A88, XXREAL_0:2;

then A93: k in Seg ((len a) * (len b)) by A92;

k in dom FG by A12, B1, A92, FINSEQ_3:25;

then A94: FG . k in rng FG by FUNCT_1:def 3;

A95: j = ((k -' 1) mod (len b)) + 1 by A81, A89, A87, NAT_D:def 2;

z in (F . i) /\ (G . j) by A73, A83, A75, A78, XBOOLE_0:def 4;

then z in FG . k by A13, A14, A90, A95, A93;

hence z in union (rng FG) by A94, TARSKI:def 4; :: thesis: verum

assume z in union (rng FG) ; :: thesis: z in dom (f + g)

then consider Y being set such that

A96: z in Y and

A97: Y in rng FG by TARSKI:def 4;

consider k being object such that

A98: k in dom FG and

A99: Y = FG . k by A97, FUNCT_1:def 3;

reconsider k = k as Element of NAT by A98;

set j = ((k -' 1) mod (len b)) + 1;

set i = ((k -' 1) div (len b)) + 1;

FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A98;

then A100: ( z in F . (((k -' 1) div (len b)) + 1) & z in G . (((k -' 1) mod (len b)) + 1) ) by A96, A99, XBOOLE_0:def 4;

A102: ( 1 <= k & k <= (len a) * (len b) ) by A12, A98, FINSEQ_3:25;

A103: len b <> 0 by A102;

then A104: len b >= 1 by NAT_1:14;

( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by A102, NAT_D:def 3, XXREAL_0:2;

then A105: (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A104, NAT_2:15;

A106: ((len a) * (len b)) div (len b) = len a by A103, NAT_D:18;

k -' 1 <= ((len a) * (len b)) -' 1 by A102, NAT_D:42;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A105, NAT_2:24;

then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then ((k -' 1) div (len b)) + 1 in dom F by A11, A106, NAT_1:11, FINSEQ_3:25;

then F . (((k -' 1) div (len b)) + 1) in rng F by FUNCT_1:def 3;

then a107: z in dom f by A51, A100, TARSKI:def 4;

( 1 <= ((k -' 1) mod (len b)) + 1 & ((k -' 1) mod (len b)) + 1 <= len b ) by A103, NAT_D:1, NAT_1:11, NAT_1:13;

then ((k -' 1) mod (len b)) + 1 in dom G by A11, FINSEQ_3:25;

then G . (((k -' 1) mod (len b)) + 1) in rng G by FUNCT_1:def 3;

then z in dom g by A70, A100, TARSKI:def 4;

hence z in dom (f + g) by A8, a107, XBOOLE_0:def 4; :: thesis: verum

for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds

(f + g) . x = (f + g) . y

proof

let k be Nat; :: thesis: for x, y being Element of X st k in dom FG & x in FG . k & y in FG . k holds

(f + g) . x = (f + g) . y

let x, y be Element of X; :: thesis: ( k in dom FG & x in FG . k & y in FG . k implies (f + g) . x = (f + g) . y )

assume that

A108: k in dom FG and

A109: ( x in FG . k & y in FG . k ) ; :: thesis: (f + g) . x = (f + g) . y

set i = ((k -' 1) div (len b)) + 1;

set j = ((k -' 1) mod (len b)) + 1;

A110: ( ((k -' 1) div (len b)) + 1 >= 1 & ((k -' 1) mod (len b)) + 1 >= 1 ) by NAT_1:11;

FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A108;

then A112: ( x in F . (((k -' 1) div (len b)) + 1) & x in G . (((k -' 1) mod (len b)) + 1) & y in F . (((k -' 1) div (len b)) + 1) & y in G . (((k -' 1) mod (len b)) + 1) ) by A109, XBOOLE_0:def 4;

A113: ( 1 <= k & k <= (len a) * (len b) ) by A12, A108, FINSEQ_3:25;

then A115: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

A116: ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by A113, NAT_D:def 3, XXREAL_0:2;

A117: len b <> 0 by A113;

then len b >= 1 by NAT_1:14;

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A116, NAT_2:15;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A115, NAT_2:24;

then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then ((k -' 1) div (len b)) + 1 <= len a by A117, NAT_D:18;

then A119: ( f . x = a . (((k -' 1) div (len b)) + 1) & f . y = a . (((k -' 1) div (len b)) + 1) ) by A10, A11, A110, A112, FINSEQ_3:25, MESFUNC3:def 1;

A120: ((k -' 1) mod (len b)) + 1 <= len b by A117, NAT_D:1, NAT_1:13;

FG . k in rng FG by A108, FUNCT_1:def 3;

then A124: ( x in dom (f + g) & y in dom (f + g) ) by A71, A109, TARSKI:def 4;

hence (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3

.= (a . (((k -' 1) div (len b)) + 1)) + (b . (((k -' 1) mod (len b)) + 1)) by A9, A11, A110, A120, A112, A119, FINSEQ_3:25, MESFUNC3:def 1

.= (f . y) + (g . y) by A9, A11, A110, A120, A112, A119, FINSEQ_3:25, MESFUNC3:def 1

.= (f + g) . y by A124, MESFUNC1:def 3 ;

:: thesis: verum

end;(f + g) . x = (f + g) . y

let x, y be Element of X; :: thesis: ( k in dom FG & x in FG . k & y in FG . k implies (f + g) . x = (f + g) . y )

assume that

A108: k in dom FG and

A109: ( x in FG . k & y in FG . k ) ; :: thesis: (f + g) . x = (f + g) . y

set i = ((k -' 1) div (len b)) + 1;

set j = ((k -' 1) mod (len b)) + 1;

A110: ( ((k -' 1) div (len b)) + 1 >= 1 & ((k -' 1) mod (len b)) + 1 >= 1 ) by NAT_1:11;

FG . k = (F . (((k -' 1) div (len b)) + 1)) /\ (G . (((k -' 1) mod (len b)) + 1)) by A13, A108;

then A112: ( x in F . (((k -' 1) div (len b)) + 1) & x in G . (((k -' 1) mod (len b)) + 1) & y in F . (((k -' 1) div (len b)) + 1) & y in G . (((k -' 1) mod (len b)) + 1) ) by A109, XBOOLE_0:def 4;

A113: ( 1 <= k & k <= (len a) * (len b) ) by A12, A108, FINSEQ_3:25;

then A115: k -' 1 <= ((len a) * (len b)) -' 1 by NAT_D:42;

A116: ( len b divides (len a) * (len b) & 1 <= (len a) * (len b) ) by A113, NAT_D:def 3, XXREAL_0:2;

A117: len b <> 0 by A113;

then len b >= 1 by NAT_1:14;

then (((len a) * (len b)) -' 1) div (len b) = (((len a) * (len b)) div (len b)) - 1 by A116, NAT_2:15;

then (k -' 1) div (len b) <= (((len a) * (len b)) div (len b)) - 1 by A115, NAT_2:24;

then ((k -' 1) div (len b)) + 1 <= ((len a) * (len b)) div (len b) by XREAL_1:19;

then ((k -' 1) div (len b)) + 1 <= len a by A117, NAT_D:18;

then A119: ( f . x = a . (((k -' 1) div (len b)) + 1) & f . y = a . (((k -' 1) div (len b)) + 1) ) by A10, A11, A110, A112, FINSEQ_3:25, MESFUNC3:def 1;

A120: ((k -' 1) mod (len b)) + 1 <= len b by A117, NAT_D:1, NAT_1:13;

FG . k in rng FG by A108, FUNCT_1:def 3;

then A124: ( x in dom (f + g) & y in dom (f + g) ) by A71, A109, TARSKI:def 4;

hence (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3

.= (a . (((k -' 1) div (len b)) + 1)) + (b . (((k -' 1) mod (len b)) + 1)) by A9, A11, A110, A120, A112, A119, FINSEQ_3:25, MESFUNC3:def 1

.= (f . y) + (g . y) by A9, A11, A110, A120, A112, A119, FINSEQ_3:25, MESFUNC3:def 1

.= (f + g) . y by A124, MESFUNC1:def 3 ;

:: thesis: verum

now :: thesis: for x being Element of X st x in dom (f + g) holds

|.((f + g) . x).| < +infty

hence
f + g is_simple_func_in S
by A71, A107, MESFUNC2:def 1, MESFUNC2:def 4; :: thesis: verum|.((f + g) . x).| < +infty

let x be Element of X; :: thesis: ( x in dom (f + g) implies |.((f + g) . x).| < +infty )

assume A188: x in dom (f + g) ; :: thesis: |.((f + g) . x).| < +infty

then |.((f + g) . x).| = |.((f . x) + (g . x)).| by MESFUNC1:def 3;

then A189: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:24;

( x in dom f & x in dom g ) by A188, A8, XBOOLE_0:def 4;

then ( |.(f . x).| < +infty & |.(g . x).| < +infty ) by A1, A4, MESFUNC2:def 1, MESFUNC2:def 4;

then |.(f . x).| + |.(g . x).| <> +infty by XXREAL_3:16;

hence |.((f + g) . x).| < +infty by A189, XXREAL_0:2, XXREAL_0:4; :: thesis: verum

end;assume A188: x in dom (f + g) ; :: thesis: |.((f + g) . x).| < +infty

then |.((f + g) . x).| = |.((f . x) + (g . x)).| by MESFUNC1:def 3;

then A189: |.((f + g) . x).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:24;

( x in dom f & x in dom g ) by A188, A8, XBOOLE_0:def 4;

then ( |.(f . x).| < +infty & |.(g . x).| < +infty ) by A1, A4, MESFUNC2:def 1, MESFUNC2:def 4;

then |.(f . x).| + |.(g . x).| <> +infty by XXREAL_3:16;

hence |.((f + g) . x).| < +infty by A189, XXREAL_0:2, XXREAL_0:4; :: thesis: verum