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:
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 ;
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 ;
then ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by ;
hence (Im f) . x = (Im f) . y by A2, A5, A6; :: thesis: verum
end;
A7: dom (Re f) = union (rng F) by ;
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 ;
then ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by ;
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 ; :: thesis: verum
end;
assume that
A10: Re f is_simple_func_in S and
A11: Im f is_simple_func_in S ; :: thesis:
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 ;
set la = len F;
A14: dom f = union (rng F) by ;
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 ;
set lb = len G;
deffunc H1( 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 = H1(k) from A19: dom FG = Seg ((len F) * (len G)) by ;
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 ;
A24: k <= (len F) * (len G) by ;
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 ;
1 <= len G by ;
then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by ;
then ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) by ;
then ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= len F ) by ;
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 ;
then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by ;
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 ;
hence FG . k in S by ; :: 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 ;
then A32: len G > 0 by ;
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 ;
then A35: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by ;
1 <= len G by ;
then A36: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by ;
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 ;
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
.= (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 ;
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 ;
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 ;
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 ;
then A39: (l - 1) + 1 = (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1) by ;
(l -' 1) mod (len G) < len G by ;
then ( ((l -' 1) mod (len G)) + 1 >= 1 & ((l -' 1) mod (len G)) + 1 <= len G ) by ;
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 ;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by ;
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 ;
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 ;
then A42: (k - 1) + 1 = (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1) by ;
(k -' 1) mod (len G) < len G by ;
then ( ((k -' 1) mod (len G)) + 1 >= 1 & ((k -' 1) mod (len G)) + 1 <= len G ) by ;
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 ) div (len G)) + 1 <> ((l -' 1) div (len G)) + 1 or ((k -' 1) mod (len G)) + 1 <> ((l -' 1) mod (len G)) + 1 ) by ;
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 ;
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 ;
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 ;
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 ;
consider Z being set such that
A49: z in Z and
A50: Z in rng G by ;
consider j being Nat such that
A51: j in dom G and
A52: Z = G . j by ;
consider i being Nat such that
A53: i in dom F and
A54: F . i = Y by ;
1 <= i by ;
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 ;
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 ;
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 ;
A59: 1 <= j by ;
then consider j9 being Nat such that
A60: j = 1 + j9 by NAT_1:10;
A61: j9 < len G by ;
A62: k >= j by ;
then A63: k -' 1 = k - 1 by
.= (i9 * (len G)) + j9 by ;
then A64: i = ((k -' 1) div (len G)) + 1 by ;
A65: k >= 1 by ;
then A66: k in Seg ((len F) * (len G)) by A58;
A67: j = ((k -' 1) mod (len G)) + 1 by ;
k in dom FG by ;
then A68: FG . k in rng FG by FUNCT_1:def 3;
z in (F . i) /\ (G . j) by ;
then z in FG . k by A18, A19, A64, A67, A66;
hence z in union (rng FG) by ; :: 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 ;
A73: 1 <= k by ;
then A74: len G > 0 by ;
then A75: 1 <= len G by NAT_1:14;
A76: k <= (len F) * (len G) by ;
then ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by ;
then A77: (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by ;
set j = ((k -' 1) mod (len G)) + 1;
set i = ((k -' 1) div (len G)) + 1;
k -' 1 <= ((len F) * (len G)) -' 1 by ;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by ;
then A78: ( ((k -' 1) div (len G)) + 1 >= 1 & ((k -' 1) div (len G)) + 1 <= ((len F) * (len G)) div (len G) ) by ;
((len F) * (len G)) div (len G) = len F by ;
then ((k -' 1) div (len G)) + 1 in dom F by ;
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 ;
then z in F . (((k -' 1) div (len G)) + 1) by ;
hence z in dom f by ; :: 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 ;
then FG . k c= dom (Im f) by ;
then A83: ( (Im f) . x = Im (f . x) & (Im f) . y = Im (f . y) ) by ;
A84: 1 <= k by ;
then A85: len G > 0 by ;
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 ;
then A86: ((k -' 1) mod (len G)) + 1 in dom G by FINSEQ_3:25;
FG . k c= dom (Re f) by ;
then A87: ( (Re f) . x = Re (f . x) & (Re f) . y = Re (f . y) ) by ;
A88: k <= (len F) * (len G) by ;
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 ;
then ( x in G . (((k -' 1) mod (len G)) + 1) & y in G . (((k -' 1) mod (len G)) + 1) ) by ;
then A91: Im (f . x) = Im (f . y) by ;
A92: ( len G divides (len F) * (len G) & 1 <= (len F) * (len G) ) by ;
1 <= len G by ;
then (((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1 by ;
then (k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1 by ;
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 ;
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 ;
then Re (f . x) = Re (f . y) by ;
hence f . x = f . y by A91; :: thesis: verum
end;
hence f is_simple_func_in S by A45; :: thesis: verum