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

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )

A10: Re f is_simple_func_in S and

A11: Im f is_simple_func_in S ; :: thesis: f is_simple_func_in S

consider F being Finite_Sep_Sequence of S such that

A12: dom (Re f) = union (rng F) and

A13: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(Re f) . x = (Re f) . y by A10, MESFUNC6:def 2;

set la = len F;

A14: dom f = union (rng F) by A12, COMSEQ_3:def 3;

consider G being Finite_Sep_Sequence of S such that

A15: dom (Im f) = union (rng G) and

A16: for n being Nat

for x, y being Element of X st n in dom G & x in G . n & y in G . n holds

(Im f) . x = (Im f) . y by A11, MESFUNC6:def 2;

set lb = len G;

deffunc H_{1}( Nat) -> set = (F . ((($1 -' 1) div (len G)) + 1)) /\ (G . ((($1 -' 1) mod (len G)) + 1));

consider FG being FinSequence such that

A17: len FG = (len F) * (len G) and

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

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

A19: dom FG = Seg ((len F) * (len G)) by A17, 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

A44: dom f = union (rng G) by A15, COMSEQ_3:def 4;

A45: dom f = 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 . x = f . y

for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX holds

( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_simple_func_in S iff ( Re f is_simple_func_in S & Im f is_simple_func_in S ) )

hereby :: thesis: ( Re f is_simple_func_in S & Im f is_simple_func_in S implies f is_simple_func_in S )

assume that assume
f is_simple_func_in S
; :: thesis: ( Re f is_simple_func_in S & Im f is_simple_func_in S )

then consider F being Finite_Sep_Sequence of S such that

A1: dom f = union (rng F) and

A2: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y ;

A3: dom (Im f) = union (rng F) by A1, COMSEQ_3:def 4;

A4: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(Im f) . x = (Im f) . y

for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(Re f) . x = (Re f) . y

end;then consider F being Finite_Sep_Sequence of S such that

A1: dom f = union (rng F) and

A2: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

f . x = f . y ;

A3: dom (Im f) = union (rng F) by A1, COMSEQ_3:def 4;

A4: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(Im f) . x = (Im f) . y

proof

A7:
dom (Re f) = union (rng F)
by A1, COMSEQ_3:def 3;
let n be Nat; :: thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(Im f) . x = (Im f) . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies (Im f) . x = (Im f) . y )

assume that

A5: n in dom F and

A6: ( x in F . n & y in F . n ) ; :: thesis: (Im f) . x = (Im f) . y

F . n c= union (rng F) by A5, MESFUNC3:7;

then ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A3, A6, COMSEQ_3:def 4;

hence (Im f) . x = (Im f) . y by A2, A5, A6; :: thesis: verum

end;(Im f) . x = (Im f) . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies (Im f) . x = (Im f) . y )

assume that

A5: n in dom F and

A6: ( x in F . n & y in F . n ) ; :: thesis: (Im f) . x = (Im f) . y

F . n c= union (rng F) by A5, MESFUNC3:7;

then ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A3, A6, COMSEQ_3:def 4;

hence (Im f) . x = (Im f) . y by A2, A5, A6; :: thesis: verum

for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(Re f) . x = (Re f) . y

proof

hence
( Re f is_simple_func_in S & Im f is_simple_func_in S )
by A7, A3, A4, MESFUNC6:def 2; :: thesis: verum
let n be Nat; :: thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(Re f) . x = (Re f) . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies (Re f) . x = (Re f) . y )

assume that

A8: n in dom F and

A9: ( x in F . n & y in F . n ) ; :: thesis: (Re f) . x = (Re f) . y

F . n c= union (rng F) by A8, MESFUNC3:7;

then ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A7, A9, COMSEQ_3:def 3;

hence (Re f) . x = (Re f) . y by A2, A8, A9; :: thesis: verum

end;(Re f) . x = (Re f) . y

let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies (Re f) . x = (Re f) . y )

assume that

A8: n in dom F and

A9: ( x in F . n & y in F . n ) ; :: thesis: (Re f) . x = (Re f) . y

F . n c= union (rng F) by A8, MESFUNC3:7;

then ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A7, A9, COMSEQ_3:def 3;

hence (Re f) . x = (Re f) . y by A2, A8, A9; :: thesis: verum

A10: Re f is_simple_func_in S and

A11: Im f is_simple_func_in S ; :: thesis: f is_simple_func_in S

consider F being Finite_Sep_Sequence of S such that

A12: dom (Re f) = union (rng F) and

A13: for n being Nat

for x, y being Element of X st n in dom F & x in F . n & y in F . n holds

(Re f) . x = (Re f) . y by A10, MESFUNC6:def 2;

set la = len F;

A14: dom f = union (rng F) by A12, COMSEQ_3:def 3;

consider G being Finite_Sep_Sequence of S such that

A15: dom (Im f) = union (rng G) and

A16: for n being Nat

for x, y being Element of X st n in dom G & x in G . n & y in G . n holds

(Im f) . x = (Im f) . y by A11, MESFUNC6:def 2;

set lb = len G;

deffunc H

consider FG being FinSequence such that

A17: len FG = (len F) * (len G) and

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

FG . k = H

A19: dom FG = Seg ((len F) * (len G)) by A17, 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 )

A20: len G divides (len F) * (len G) by NAT_D:def 3;

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

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

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

then A22: 1 <= k by FINSEQ_3:25;

then A23: len G > 0 by A17, A21, FINSEQ_3:25;

A24: k <= (len F) * (len G) by A17, A21, FINSEQ_3:25;

then k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

then A25: (k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G) by NAT_2:24;

A26: 1 <= (len F) * (len G) by A22, A24, XXREAL_0:2;

1 <= len G by A23, NAT_1:14;

then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A26, A20, NAT_2:15;

then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A25, XREAL_1:19;

then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A23, NAT_1:14, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25;

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

(k -' 1) mod (len G) < len G by A23, NAT_D:1;

then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;

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

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

then (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S by A27, MEASURE1:34;

hence FG . k in S by A18, A21; :: thesis: verum

end;A20: len G divides (len F) * (len G) by NAT_D:def 3;

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

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

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

then A22: 1 <= k by FINSEQ_3:25;

then A23: len G > 0 by A17, A21, FINSEQ_3:25;

A24: k <= (len F) * (len G) by A17, A21, FINSEQ_3:25;

then k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

then A25: (k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G) by NAT_2:24;

A26: 1 <= (len F) * (len G) by A22, A24, XXREAL_0:2;

1 <= len G by A23, NAT_1:14;

then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A26, A20, NAT_2:15;

then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by A25, XREAL_1:19;

then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A23, NAT_1:14, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25;

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

(k -' 1) mod (len G) < len G by A23, NAT_D:1;

then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;

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

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

then (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S by A27, MEASURE1:34;

hence FG . k in S by A18, A21; :: 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

A28: k in dom FG and

A29: l in dom FG and

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

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

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

A31: 1 <= k by A28, FINSEQ_3:25;

then A32: len G > 0 by A17, A28, FINSEQ_3:25;

then A33: (l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1 by NAT_D:2;

A34: k <= (len F) * (len G) by A17, A28, FINSEQ_3:25;

then A35: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A31, NAT_1:14, NAT_D:def 3;

1 <= len G by A32, NAT_1:14;

then A36: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A35, NAT_2:15;

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

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

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

then A37: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A18, A29

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

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

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

l <= (len F) * (len G) by A17, A29, FINSEQ_3:25;

then l -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

then (l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24;

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

then ( ((l -' 1) div (len G)) + 1 >= 1 & ((l -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:14, NAT_D:18;

then ((l -' 1) div (len G)) + 1 in Seg (len F) ;

then A38: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

1 <= l by A29, FINSEQ_3:25;

then A39: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A33, XREAL_1:233;

(l -' 1) mod (len G) < len G by A32, NAT_D:1;

then ( ((l -' 1) mod (len G)) + 1 >= 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;

then ((l -' 1) mod (len G)) + 1 in Seg (len G) ;

then A40: ((l -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def 3;

k -' 1 <= ((len F) * (len G)) -' 1 by A34, NAT_D:42;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24;

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

then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:11, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in Seg (len F) ;

then A41: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

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

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

(k -' 1) mod (len G) < len G by A32, NAT_D:1;

then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:11, NAT_1:13;

then ((k -' 1) mod (len G)) + 1 in Seg (len G) ;

then A43: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def 3;

end;assume that

A28: k in dom FG and

A29: l in dom FG and

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

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

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

A31: 1 <= k by A28, FINSEQ_3:25;

then A32: len G > 0 by A17, A28, FINSEQ_3:25;

then A33: (l -' 1) + 1 = ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1 by NAT_D:2;

A34: k <= (len F) * (len G) by A17, A28, FINSEQ_3:25;

then A35: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A31, NAT_1:14, NAT_D:def 3;

1 <= len G by A32, NAT_1:14;

then A36: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A35, NAT_2:15;

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

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

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

then A37: (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))) /\ ((F . (((l -' 1) div (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A18, A29

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

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

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

l <= (len F) * (len G) by A17, A29, FINSEQ_3:25;

then l -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

then (l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24;

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

then ( ((l -' 1) div (len G)) + 1 >= 1 & ((l -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:14, NAT_D:18;

then ((l -' 1) div (len G)) + 1 in Seg (len F) ;

then A38: ((l -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

1 <= l by A29, FINSEQ_3:25;

then A39: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by A33, XREAL_1:233;

(l -' 1) mod (len G) < len G by A32, NAT_D:1;

then ( ((l -' 1) mod (len G)) + 1 >= 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;

then ((l -' 1) mod (len G)) + 1 in Seg (len G) ;

then A40: ((l -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def 3;

k -' 1 <= ((len F) * (len G)) -' 1 by A34, NAT_D:42;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A36, NAT_2:24;

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

then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A32, NAT_1:11, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in Seg (len F) ;

then A41: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_1:def 3;

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

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

(k -' 1) mod (len G) < len G by A32, NAT_D:1;

then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:11, NAT_1:13;

then ((k -' 1) mod (len G)) + 1 in Seg (len G) ;

then A43: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_1:def 3;

per cases
( ((k -' 1) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 or ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 )
by A30, A42, A39;

end;

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

then
F . (((k -' 1) div (len G)) + 1) misses F . (((l -' 1) div (len G)) + 1)
by A41, A38, MESFUNC3:4;

then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A37;

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

end;then (FG . k) /\ (FG . l) = {} /\ ((G . (((k -' 1) mod (len G)) + 1)) /\ (G . (((l -' 1) mod (len G)) + 1))) by A37;

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

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

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

then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A37;

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

end;then (FG . k) /\ (FG . l) = ((F . (((k -' 1) div (len G)) + 1)) /\ (F . (((l -' 1) div (len G)) + 1))) /\ {} by A37;

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

A44: dom f = union (rng G) by A15, COMSEQ_3:def 4;

A45: dom f = union (rng FG)

proof

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

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

then consider Y being set such that

A69: z in Y and

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

consider k being Nat such that

A71: k in dom FG and

A72: FG . k = Y by A70, FINSEQ_2:10;

A73: 1 <= k by A71, FINSEQ_3:25;

then A74: len G > 0 by A17, A71, FINSEQ_3:25;

then A75: 1 <= len G by NAT_1:14;

A76: k <= (len F) * (len G) by A17, A71, FINSEQ_3:25;

then ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A73, NAT_1:14, NAT_D:def 3;

then A77: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A75, NAT_2:15;

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

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

k -' 1 <= ((len F) * (len G)) -' 1 by A76, NAT_D:42;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A77, NAT_2:24;

then A78: ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) ) by NAT_1:14, XREAL_1:19;

((len F) * (len G)) div (len G) = len F by A74, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in dom F by A78, FINSEQ_3:25;

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

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

then z in F . (((k -' 1) div (len G)) + 1) by A69, A72, XBOOLE_0:def 4;

hence z in dom f by A14, A79, TARSKI: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 )
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in dom f or z in union (rng FG) )

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

then consider Y being set such that

A47: z in Y and

A48: Y in rng F by A14, TARSKI:def 4;

consider Z being set such that

A49: z in Z and

A50: Z in rng G by A44, A46, TARSKI:def 4;

consider j being Nat such that

A51: j in dom G and

A52: Z = G . j by A50, FINSEQ_2:10;

consider i being Nat such that

A53: i in dom F and

A54: F . i = Y by A48, FINSEQ_2:10;

1 <= i by A53, FINSEQ_3:25;

then consider i9 being Nat such that

A55: i = 1 + i9 by NAT_1:10;

set k = ((i - 1) * (len G)) + j;

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

i <= len F by A53, FINSEQ_3:25;

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

then (i - 1) * (len G) <= ((len F) - 1) * (len G) by XREAL_1:64;

then A56: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6;

A57: j <= len G by A51, FINSEQ_3:25;

then (((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by XREAL_1:6;

then A58: k <= (len F) * (len G) by A56, XXREAL_0:2;

A59: 1 <= j by A51, FINSEQ_3:25;

then consider j9 being Nat such that

A60: j = 1 + j9 by NAT_1:10;

A61: j9 < len G by A57, A60, NAT_1:13;

A62: k >= j by A55, NAT_1:11;

then A63: k -' 1 = k - 1 by A59, XREAL_1:233, XXREAL_0:2

.= (i9 * (len G)) + j9 by A55, A60 ;

then A64: i = ((k -' 1) div (len G)) + 1 by A55, A61, NAT_D:def 1;

A65: k >= 1 by A59, A62, XXREAL_0:2;

then A66: k in Seg ((len F) * (len G)) by A58;

A67: j = ((k -' 1) mod (len G)) + 1 by A60, A63, A61, NAT_D:def 2;

k in dom FG by A17, A65, A58, FINSEQ_3:25;

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

z in (F . i) /\ (G . j) by A47, A54, A49, A52, XBOOLE_0:def 4;

then z in FG . k by A18, A19, A64, A67, A66;

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

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

then consider Y being set such that

A47: z in Y and

A48: Y in rng F by A14, TARSKI:def 4;

consider Z being set such that

A49: z in Z and

A50: Z in rng G by A44, A46, TARSKI:def 4;

consider j being Nat such that

A51: j in dom G and

A52: Z = G . j by A50, FINSEQ_2:10;

consider i being Nat such that

A53: i in dom F and

A54: F . i = Y by A48, FINSEQ_2:10;

1 <= i by A53, FINSEQ_3:25;

then consider i9 being Nat such that

A55: i = 1 + i9 by NAT_1:10;

set k = ((i - 1) * (len G)) + j;

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

i <= len F by A53, FINSEQ_3:25;

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

then (i - 1) * (len G) <= ((len F) - 1) * (len G) by XREAL_1:64;

then A56: k <= (((len F) - 1) * (len G)) + j by XREAL_1:6;

A57: j <= len G by A51, FINSEQ_3:25;

then (((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G) by XREAL_1:6;

then A58: k <= (len F) * (len G) by A56, XXREAL_0:2;

A59: 1 <= j by A51, FINSEQ_3:25;

then consider j9 being Nat such that

A60: j = 1 + j9 by NAT_1:10;

A61: j9 < len G by A57, A60, NAT_1:13;

A62: k >= j by A55, NAT_1:11;

then A63: k -' 1 = k - 1 by A59, XREAL_1:233, XXREAL_0:2

.= (i9 * (len G)) + j9 by A55, A60 ;

then A64: i = ((k -' 1) div (len G)) + 1 by A55, A61, NAT_D:def 1;

A65: k >= 1 by A59, A62, XXREAL_0:2;

then A66: k in Seg ((len F) * (len G)) by A58;

A67: j = ((k -' 1) mod (len G)) + 1 by A60, A63, A61, NAT_D:def 2;

k in dom FG by A17, A65, A58, FINSEQ_3:25;

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

z in (F . i) /\ (G . j) by A47, A54, A49, A52, XBOOLE_0:def 4;

then z in FG . k by A18, A19, A64, A67, A66;

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

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

then consider Y being set such that

A69: z in Y and

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

consider k being Nat such that

A71: k in dom FG and

A72: FG . k = Y by A70, FINSEQ_2:10;

A73: 1 <= k by A71, FINSEQ_3:25;

then A74: len G > 0 by A17, A71, FINSEQ_3:25;

then A75: 1 <= len G by NAT_1:14;

A76: k <= (len F) * (len G) by A17, A71, FINSEQ_3:25;

then ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A73, NAT_1:14, NAT_D:def 3;

then A77: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A75, NAT_2:15;

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

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

k -' 1 <= ((len F) * (len G)) -' 1 by A76, NAT_D:42;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A77, NAT_2:24;

then A78: ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) ) by NAT_1:14, XREAL_1:19;

((len F) * (len G)) div (len G) = len F by A74, NAT_D:18;

then ((k -' 1) div (len G)) + 1 in dom F by A78, FINSEQ_3:25;

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

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

then z in F . (((k -' 1) div (len G)) + 1) by A69, A72, XBOOLE_0:def 4;

hence z in dom f by A14, A79, TARSKI: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 . x = f . y

proof

hence
f is_simple_func_in S
by A45; :: thesis: verum
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 . x = f . y

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

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

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

assume that

A80: k in dom FG and

A81: ( x in FG . k & y in FG . k ) ; :: thesis: f . x = f . y

A82: FG . k c= union (rng FG) by A80, MESFUNC3:7;

then FG . k c= dom (Im f) by A45, COMSEQ_3:def 4;

then A83: ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A81, COMSEQ_3:def 4;

A84: 1 <= k by A80, FINSEQ_3:25;

then A85: len G > 0 by A17, A80, FINSEQ_3:25;

then (k -' 1) mod (len G) < len G by NAT_D:1;

then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;

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

FG . k c= dom (Re f) by A45, A82, COMSEQ_3:def 3;

then A87: ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A81, COMSEQ_3:def 3;

A88: k <= (len F) * (len G) by A17, A80, FINSEQ_3:25;

then A89: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

A90: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A80;

then ( x in G . (((k -' 1) mod (len G)) + 1) & y in G . (((k -' 1) mod (len G)) + 1) ) by A81, XBOOLE_0:def 4;

then A91: Im (f . x) = Im (f . y) by A16, A86, A83;

A92: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A84, A88, NAT_1:14, NAT_D:def 3;

1 <= len G by A85, NAT_1:14;

then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A92, NAT_2:15;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A89, NAT_2:24;

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

then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A85, NAT_1:14, NAT_D:18;

then A93: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25;

( x in F . (((k -' 1) div (len G)) + 1) & y in F . (((k -' 1) div (len G)) + 1) ) by A81, A90, XBOOLE_0:def 4;

then Re (f . x) = Re (f . y) by A13, A93, A87;

hence f . x = f . y by A91; :: thesis: verum

end;f . x = f . y

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

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

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

assume that

A80: k in dom FG and

A81: ( x in FG . k & y in FG . k ) ; :: thesis: f . x = f . y

A82: FG . k c= union (rng FG) by A80, MESFUNC3:7;

then FG . k c= dom (Im f) by A45, COMSEQ_3:def 4;

then A83: ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by A81, COMSEQ_3:def 4;

A84: 1 <= k by A80, FINSEQ_3:25;

then A85: len G > 0 by A17, A80, FINSEQ_3:25;

then (k -' 1) mod (len G) < len G by NAT_D:1;

then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by NAT_1:13, NAT_1:14;

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

FG . k c= dom (Re f) by A45, A82, COMSEQ_3:def 3;

then A87: ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by A81, COMSEQ_3:def 3;

A88: k <= (len F) * (len G) by A17, A80, FINSEQ_3:25;

then A89: k -' 1 <= ((len F) * (len G)) -' 1 by NAT_D:42;

A90: FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) by A18, A80;

then ( x in G . (((k -' 1) mod (len G)) + 1) & y in G . (((k -' 1) mod (len G)) + 1) ) by A81, XBOOLE_0:def 4;

then A91: Im (f . x) = Im (f . y) by A16, A86, A83;

A92: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by A84, A88, NAT_1:14, NAT_D:def 3;

1 <= len G by A85, NAT_1:14;

then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by A92, NAT_2:15;

then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by A89, NAT_2:24;

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

then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by A85, NAT_1:14, NAT_D:18;

then A93: ((k -' 1) div (len G)) + 1 in dom F by FINSEQ_3:25;

( x in F . (((k -' 1) div (len G)) + 1) & y in F . (((k -' 1) div (len G)) + 1) ) by A81, A90, XBOOLE_0:def 4;

then Re (f . x) = Re (f . y) by A13, A93, A87;

hence f . x = f . y by A91; :: thesis: verum