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 ) )
assume AS:
( Re f is_simple_func_in S & Im f is_simple_func_in S )
; :: thesis: f is_simple_func_in S
then consider F being Finite_Sep_Sequence of S such that
A1:
( dom (Re f) = union (rng F) & ( 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 MESFUNC6:def 7;
consider G being Finite_Sep_Sequence of S such that
A2:
( dom (Im f) = union (rng G) & ( 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 AS, MESFUNC6:def 7;
A3:
( dom f = union (rng F) & dom f = union (rng G) )
by A1, A2, MESFUN6C:def 1, MESFUN6C:def 2;
set la = len F;
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
A13:
len FG = (len F) * (len G)
and
A14:
for k being Nat st k in dom FG holds
FG . k = H1(k)
from FINSEQ_1:sch 2();
A15:
dom FG = Seg ((len F) * (len G))
by A13, FINSEQ_1:def 3;
now let k be
Nat;
:: thesis: ( k in dom FG implies FG . k in S )assume B16:
k in dom FG
;
:: thesis: FG . k in Sthen A19:
( 1
<= k &
k <= (len F) * (len G) )
by A13, FINSEQ_3:27;
then A20:
len G > 0
;
then P3:
1
<= len G
by NAT_1:14;
P2:
1
<= (len F) * (len G)
by A19, XXREAL_0:2;
len G divides (len F) * (len G)
by NAT_D:def 3;
then A22:
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by P2, P3, NAT_2:17;
set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
A18:
(
((k -' 1) div (len G)) + 1
>= 1 &
((k -' 1) mod (len G)) + 1
>= 1 )
by NAT_1:14;
k -' 1
<= ((len F) * (len G)) -' 1
by A19, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) -' 1) div (len G)
by NAT_2:26;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by A22, XREAL_1:21;
then
((k -' 1) div (len G)) + 1
<= len F
by A20, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in dom F
by A18, FINSEQ_3:27;
then A30:
F . (((k -' 1) div (len G)) + 1) in rng F
by FUNCT_1:12;
(k -' 1) mod (len G) < len G
by A20, NAT_D:1;
then
((k -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
then
((k -' 1) mod (len G)) + 1
in dom G
by A18, FINSEQ_3:27;
then
G . (((k -' 1) mod (len G)) + 1) in rng G
by FUNCT_1:12;
then
(F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1)) in S
by A30, MEASURE1:66;
hence
FG . k in S
by A14, B16;
:: thesis: verum end;
then reconsider FG = FG as FinSequence of S by FINSEQ_2:14;
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 A33:
(
k in dom FG &
l in dom FG &
k <> l )
;
:: thesis: FG . k misses FG . l
set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
set n =
((l -' 1) div (len G)) + 1;
set m =
((l -' 1) mod (len G)) + 1;
A38:
( 1
<= k &
k <= (len F) * (len G) & 1
<= l &
l <= (len F) * (len G) )
by A13, A33, FINSEQ_3:27;
A37:
(
((k -' 1) div (len G)) + 1
>= 1 &
((k -' 1) mod (len G)) + 1
>= 1 )
by NAT_1:11;
A39:
len G > 0
by A38;
then
(
len G divides (len F) * (len G) & 1
<= (len F) * (len G) & 1
<= len G )
by A38, NAT_1:14, NAT_D:def 3;
then A41:
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by NAT_2:17;
k -' 1
<= ((len F) * (len G)) -' 1
by A38, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A41, NAT_2:26;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:21;
then
((k -' 1) div (len G)) + 1
<= len F
by A39, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in Seg (len F)
by A37;
then A45:
((k -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
(k -' 1) mod (len G) < len G
by A39, NAT_D:1;
then
((k -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
then
((k -' 1) mod (len G)) + 1
in Seg (len G)
by A37;
then A46:
((k -' 1) mod (len G)) + 1
in dom G
by FINSEQ_1:def 3;
A47:
(
((l -' 1) div (len G)) + 1
>= 1 &
((l -' 1) mod (len G)) + 1
>= 1 )
by NAT_1:14;
l -' 1
<= ((len F) * (len G)) -' 1
by A38, NAT_D:42;
then
(l -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A41, NAT_2:26;
then
((l -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:21;
then
((l -' 1) div (len G)) + 1
<= len F
by A39, NAT_D:18;
then
((l -' 1) div (len G)) + 1
in Seg (len F)
by A47;
then A51:
((l -' 1) div (len G)) + 1
in dom F
by FINSEQ_1:def 3;
(l -' 1) mod (len G) < len G
by A39, NAT_D:1;
then
((l -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
then
((l -' 1) mod (len G)) + 1
in Seg (len G)
by A47;
then A52:
((l -' 1) mod (len G)) + 1
in dom G
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 A39, NAT_D:2;
then A55:
(k - 1) + 1
= (((((k -' 1) div (len G)) + 1) - 1) * (len G)) + (((k -' 1) mod (len G)) + 1)
by A38, XREAL_1:235;
(l -' 1) + 1
= ((((((l -' 1) div (len G)) + 1) - 1) * (len G)) + ((((l -' 1) mod (len G)) + 1) - 1)) + 1
by A39, NAT_D:2;
then A54:
(l - 1) + 1
= (((((l -' 1) div (len G)) + 1) - 1) * (len G)) + (((l -' 1) mod (len G)) + 1)
by A38, XREAL_1:235;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A14, A33;
then A35:
(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 A14, A33
.=
(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
;
end;
then reconsider FG = FG as Finite_Sep_Sequence of S by MESFUNC3:4;
A80:
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 fproof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in dom f or z in union (rng FG) )
assume A81:
z in dom f
;
:: thesis: z in union (rng FG)
then consider Y being
set such that A82:
(
z in Y &
Y in rng F )
by A3, TARSKI:def 4;
consider i being
Nat such that A83:
(
i in dom F &
F . i = Y )
by A82, FINSEQ_2:11;
consider Z being
set such that A84:
(
z in Z &
Z in rng G )
by A3, A81, TARSKI:def 4;
consider j being
Nat such that A85:
(
j in dom G &
Z = G . j )
by A84, FINSEQ_2:11;
set k =
((i - 1) * (len G)) + j;
A86:
( 1
<= i &
i <= len F )
by A83, FINSEQ_3:27;
then consider i' being
Nat such that A87:
i = 1
+ i'
by NAT_1:10;
reconsider k =
((i - 1) * (len G)) + j as
Nat by A87;
A88:
( 1
<= j &
j <= len G )
by A85, FINSEQ_3:27;
then consider j' being
Nat such that A89:
j = 1
+ j'
by NAT_1:10;
A90:
k >= j
by A87, NAT_1:11;
then A91:
k >= 1
by A88, XXREAL_0:2;
A92:
k -' 1 =
k - 1
by A88, A90, XREAL_1:235, XXREAL_0:2
.=
(i' * (len G)) + j'
by A87, A89
;
A93:
j' < len G
by A88, A89, NAT_1:13;
then A94:
i = ((k -' 1) div (len G)) + 1
by A87, A92, NAT_D:def 1;
A95:
j = ((k -' 1) mod (len G)) + 1
by A89, A92, A93, NAT_D:def 2;
i - 1
<= (len F) - 1
by A86, XREAL_1:11;
then
(i - 1) * (len G) <= ((len F) - 1) * (len G)
by XREAL_1:66;
then A96:
k <= (((len F) - 1) * (len G)) + j
by XREAL_1:8;
(((len F) - 1) * (len G)) + j <= (((len F) - 1) * (len G)) + (len G)
by A88, XREAL_1:8;
then A98:
k <= (len F) * (len G)
by A96, XXREAL_0:2;
then A97:
k in Seg ((len F) * (len G))
by A91, FINSEQ_1:3;
z in (F . i) /\ (G . j)
by A82, A83, A84, A85, XBOOLE_0:def 4;
then A99:
z in FG . k
by A14, A94, A95, A97, A15;
k in dom FG
by A13, A91, A98, FINSEQ_3:27;
then
FG . k in rng FG
by FUNCT_1:def 5;
hence
z in union (rng FG)
by A99, TARSKI:def 4;
:: thesis: verum
end;
let z be
set ;
:: 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 A100:
(
z in Y &
Y in rng FG )
by TARSKI:def 4;
consider k being
Nat such that A101:
(
k in dom FG &
FG . k = Y )
by A100, FINSEQ_2:11;
set i =
((k -' 1) div (len G)) + 1;
set j =
((k -' 1) mod (len G)) + 1;
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A14, A101;
then A102:
z in F . (((k -' 1) div (len G)) + 1)
by A100, A101, XBOOLE_0:def 4;
A104:
(
((k -' 1) div (len G)) + 1
>= 1 &
((k -' 1) mod (len G)) + 1
>= 1 )
by NAT_1:14;
A103:
( 1
<= k &
k <= (len F) * (len G) )
by A13, A101, FINSEQ_3:27;
then A105:
len G > 0
;
then
(
len G divides (len F) * (len G) & 1
<= (len F) * (len G) & 1
<= len G )
by A103, NAT_1:14, NAT_D:def 3;
then A106:
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by NAT_2:17;
k -' 1
<= ((len F) * (len G)) -' 1
by A103, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A106, NAT_2:26;
then A107:
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:21;
((len F) * (len G)) div (len G) = len F
by A105, NAT_D:18;
then
((k -' 1) div (len G)) + 1
in dom F
by A104, A107, FINSEQ_3:27;
then
F . (((k -' 1) div (len G)) + 1) in rng F
by FUNCT_1:def 5;
hence
z in dom f
by A3, A102, 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 . ylet 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 A116:
(
k in dom FG &
x in FG . k &
y in FG . k )
;
:: thesis: f . x = f . y
then
FG . k = (F . (((k -' 1) div (len G)) + 1)) /\ (G . (((k -' 1) mod (len G)) + 1))
by A14;
then A127:
(
x in F . (((k -' 1) div (len G)) + 1) &
x in G . (((k -' 1) mod (len G)) + 1) &
y in F . (((k -' 1) div (len G)) + 1) &
y in G . (((k -' 1) mod (len G)) + 1) )
by A116, XBOOLE_0:def 4;
A118:
( 1
<= k &
k <= (len F) * (len G) )
by A13, A116, FINSEQ_3:27;
A119:
(
((k -' 1) div (len G)) + 1
>= 1 &
((k -' 1) mod (len G)) + 1
>= 1 )
by NAT_1:14;
A121:
len G > 0
by A118;
then
(
len G divides (len F) * (len G) & 1
<= (len F) * (len G) & 1
<= len G )
by A118, NAT_1:14, NAT_D:def 3;
then A122:
(((len F) * (len G)) -' 1) div (len G) = (((len F) * (len G)) div (len G)) - 1
by NAT_2:17;
k -' 1
<= ((len F) * (len G)) -' 1
by A118, NAT_D:42;
then
(k -' 1) div (len G) <= (((len F) * (len G)) div (len G)) - 1
by A122, NAT_2:26;
then
((k -' 1) div (len G)) + 1
<= ((len F) * (len G)) div (len G)
by XREAL_1:21;
then
((k -' 1) div (len G)) + 1
<= len F
by A121, NAT_D:18;
then A125:
((k -' 1) div (len G)) + 1
in dom F
by A119, FINSEQ_3:27;
(k -' 1) mod (len G) < len G
by A121, NAT_D:1;
then
((k -' 1) mod (len G)) + 1
<= len G
by NAT_1:13;
then A126:
((k -' 1) mod (len G)) + 1
in dom G
by A119, FINSEQ_3:27;
FG . k c= union (rng FG)
by A116, MESFUNC3:7;
then
(
FG . k c= dom (Re f) &
FG . k c= dom (Im f) )
by A80, MESFUN6C:def 1, MESFUN6C:def 2;
then
(
(Re f) . x = Re (f . x) &
(Re f) . y = Re (f . y) &
(Im f) . x = Im (f . x) &
(Im f) . y = Im (f . y) )
by A116, MESFUN6C:def 1, MESFUN6C:def 2;
then
(
Re (f . x) = Re (f . y) &
Im (f . x) = Im (f . y) )
by A1, A125, A127, A2, A126;
hence
f . x = f . y
by COMPLEX1:def 5;
:: thesis: verum
end;
hence
f is_simple_func_in S
by A80, MES2def5; :: thesis: verum