let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( f is_simple_func_in S implies f | A is_simple_func_in S )
assume f is_simple_func_in S ; :: thesis: 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 H₁( 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 = H₁(n) ) ) from FINSEQ_1:sch 2();
A4: rng G c= S

proof

let P be object ; :: according to TARSKI:def 3 :: thesis: ( not P in rng G or P in S )
assume P in rng G ; :: thesis: P in S
then consider k being object such that
A5: k in dom G and
A6: P = G . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A5;
k in Seg (len F) by A3, A5, FINSEQ_1:def 3;
then k in dom F by FINSEQ_1:def 3;
then A7: F . k in rng F by FUNCT_1:3;
G . k = (F . k) /\ A by A3, A5;
hence P in S by A6, A7, FINSUB_1:def 2; :: thesis: verum

end;

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

proof

let i, j be Nat; :: thesis: ( i in dom G & j in dom G & i <> j implies G . i misses G . j )
assume that
A9: i in dom G and
A10: j in dom G and
A11: i <> j ; :: thesis: G . i misses G . j
j in Seg (len F) by A3, A10, FINSEQ_1:def 3;
then A12: j in dom F by FINSEQ_1:def 3;
i in Seg (len F) by A3, A9, FINSEQ_1:def 3;
then i in dom F by FINSEQ_1:def 3;
then A13: F . i misses F . j by A11, A12, MESFUNC3:4;
( G . i = (F . i) /\ A & G . j = (F . j) /\ A ) by A3, A9, A10;
then (G . i) /\ (G . j) = (((F . i) /\ A) /\ (F . j)) /\ A by XBOOLE_1:16
.= (((F . i) /\ (F . j)) /\ A) /\ A by XBOOLE_1:16
.= ({} /\ A) /\ A by A13 ;
hence G . i misses G . j ; :: thesis: verum

end;

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 ; :: thesis: ( v in union (rng G) implies v in dom (f | A) )
assume v in union (rng G) ; :: thesis: 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; :: thesis: 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 ; :: thesis: ( v in dom (f | A) implies v in union (rng G) )
assume v in dom (f | A) ; :: thesis: 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; :: thesis: 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; :: thesis: 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
let x, y be Element of X; :: thesis: ( 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 ; :: thesis: (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; :: thesis: verum

end;

hence f | A is_simple_func_in S by A30; :: thesis: verum