let X be non empty set ; for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let S be SigmaField of X; for f being PartFunc of X,REAL
for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let f be PartFunc of X,REAL; for A being Element of S st f is_simple_func_in S holds
f | A is_simple_func_in S
let A be Element of S; ( f is_simple_func_in S implies f | A is_simple_func_in S )
assume
f is_simple_func_in S
; f | A 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
;
deffunc H1( Nat) -> Element of bool X = (F . $1) /\ A;
consider G being FinSequence such that
A3:
( len G = len F & ( for n being Nat st n in dom G holds
G . n = H1(n) ) )
from FINSEQ_1:sch 2();
A4:
rng G c= S
A8:
dom G = Seg (len F)
by A3, FINSEQ_1:def 3;
reconsider G = G as FinSequence of S by A4, FINSEQ_1:def 4;
for i, j being Nat st i in dom G & j in dom G & i <> j holds
G . i misses G . j
then reconsider G = G as Finite_Sep_Sequence of S by MESFUNC3:4;
for v being object st v in union (rng G) holds
v in dom (f | A)
proof
let v be
object ;
( v in union (rng G) implies v in dom (f | A) )
assume
v in union (rng G)
;
v in dom (f | A)
then consider W being
set such that A14:
v in W
and A15:
W in rng G
by TARSKI:def 4;
consider k being
object such that A16:
k in dom G
and A17:
W = G . k
by A15, FUNCT_1:def 3;
reconsider k =
k as
Element of
NAT by A16;
k in Seg (len F)
by A3, A16, FINSEQ_1:def 3;
then
k in dom F
by FINSEQ_1:def 3;
then A18:
F . k in rng F
by FUNCT_1:3;
A19:
G . k = (F . k) /\ A
by A3, A16;
then
v in F . k
by A14, A17, XBOOLE_0:def 4;
then A20:
v in union (rng F)
by A18, TARSKI:def 4;
v in A
by A14, A17, A19, XBOOLE_0:def 4;
then
v in (dom f) /\ A
by A1, A20, XBOOLE_0:def 4;
hence
v in dom (f | A)
by RELAT_1:61;
verum
end;
then A21:
union (rng G) c= dom (f | A)
;
for v being object st v in dom (f | A) holds
v in union (rng G)
proof
let v be
object ;
( v in dom (f | A) implies v in union (rng G) )
assume
v in dom (f | A)
;
v in union (rng G)
then A22:
v in (dom f) /\ A
by RELAT_1:61;
then A23:
v in A
by XBOOLE_0:def 4;
v in dom f
by A22, XBOOLE_0:def 4;
then consider W being
set such that A24:
v in W
and A25:
W in rng F
by A1, TARSKI:def 4;
consider k being
object such that A26:
k in dom F
and A27:
W = F . k
by A25, FUNCT_1:def 3;
reconsider k =
k as
Element of
NAT by A26;
A28:
k in Seg (len F)
by A26, FINSEQ_1:def 3;
then
k in dom G
by A3, FINSEQ_1:def 3;
then A29:
G . k in rng G
by FUNCT_1:3;
G . k = (F . k) /\ A
by A3, A8, A28;
then
v in G . k
by A23, A24, A27, XBOOLE_0:def 4;
hence
v in union (rng G)
by A29, TARSKI:def 4;
verum
end;
then
dom (f | A) c= union (rng G)
;
then A30:
dom (f | A) = union (rng G)
by A21;
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
(f | A) . x = (f | A) . y
proof
let n be
Nat;
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | A) . x = (f | A) . ylet x,
y be
Element of
X;
( n in dom G & x in G . n & y in G . n implies (f | A) . x = (f | A) . y )
assume that A31:
n in dom G
and A32:
x in G . n
and A33:
y in G . n
;
(f | A) . x = (f | A) . y
n in Seg (len F)
by A3, A31, FINSEQ_1:def 3;
then A34:
n in dom F
by FINSEQ_1:def 3;
G . n = (F . n) /\ A
by A3, A31;
then
(
x in F . n &
y in F . n )
by A32, A33, XBOOLE_0:def 4;
then A35:
f . x = f . y
by A2, A34;
A36:
G . n in rng G
by A31, FUNCT_1:3;
then
x in dom (f | A)
by A30, A32, TARSKI:def 4;
then A37:
(f | A) . x = f . y
by A35, FUNCT_1:47;
y in dom (f | A)
by A30, A33, A36, TARSKI:def 4;
hence
(f | A) . x = (f | A) . y
by A37, FUNCT_1:47;
verum
end;
hence
f | A is_simple_func_in S
by A30; verum