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

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

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

proof

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;

A7: dom (Re f) = union (rng F) by A1, COMSEQ_3:def 3;
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

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;

hence ( Re f is_simple_func_in S & Im f is_simple_func_in S ) by A7, A3, A4, MESFUNC6:def 2; :: thesis: verum

end;

assume that
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₁( 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₁(k) from FINSEQ_1:sch 2();
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

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;

then reconsider FG = FG as FinSequence of S by FINSEQ_2:12;
for k, l being Nat st k in dom FG & l in dom FG & k <> l holds
FG . k misses FG . l

proof

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;

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;

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;

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;

end;

end;

then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A44: dom f = union (rng G) by A15, COMSEQ_3:def 4;
A45: dom f = union (rng FG)

proof

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

proof

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;

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

for k being Nat
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

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;

hence f is_simple_func_in S by A45; :: thesis: verum