let X be non empty set ; for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) )
let S be SigmaField of X; for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) )
let f be PartFunc of X,COMPLEX; ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex c being FinSequence of COMPLEX st
( dom f = union (rng F) & dom F = dom c & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n ) & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n ) ) )
given F being Finite_Sep_Sequence of S, c being FinSequence of COMPLEX such that A4:
dom f = union (rng F)
and
A5:
dom F = dom c
and
A6:
for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Re f) . x = (Re c) . n
and
A7:
for n being Nat st n in dom F holds
for x being set st x in F . n holds
(Im f) . x = (Im c) . n
; f is_simple_func_in S
A8:
dom (Im f) = union (rng F)
by A4, COMSEQ_3:def 4;
len (Im c) = len c
by COMPLSP2:48;
then
dom (Im c) = Seg (len c)
by FINSEQ_1:def 3;
then A9:
dom F = dom (Im c)
by A5, FINSEQ_1:def 3;
len (Re c) = len c
by COMPLSP2:48;
then
dom (Re c) = Seg (len c)
by FINSEQ_1:def 3;
then A10:
dom F = dom (Re c)
by A5, FINSEQ_1:def 3;
A11:
dom (Re f) = union (rng F)
by A4, COMSEQ_3:def 3;
for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = c . n
proof
let n be
Nat;
( n in dom F implies for x being set st x in F . n holds
f . x = c . n )
assume A12:
n in dom F
;
for x being set st x in F . n holds
f . x = c . n
let x be
set ;
( x in F . n implies f . x = c . n )
assume A13:
x in F . n
;
f . x = c . n
A14:
F . n c= union (rng F)
by A12, MESFUNC3:7;
then
x in dom (Im f)
by A8, A13;
then A15:
(Im f) . x = Im (f . x)
by COMSEQ_3:def 4;
x in dom (Re f)
by A11, A13, A14;
then A16:
(Re f) . x = Re (f . x)
by COMSEQ_3:def 3;
(Im f) . x = (Im c) . n
by A7, A12, A13;
then A17:
Im (f . x) = Im (c . n)
by A9, A12, A15, Th47;
(Re f) . x = (Re c) . n
by A6, A12, A13;
then
Re (f . x) = Re (c . n)
by A10, A12, A16, Th46;
hence
f . x = c . n
by A17;
verum
end;
then
F,c are_Re-presentation_of f
by A4, A5;
hence
f is_simple_func_in S
by Th45; verum