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 by Def7;
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: dom G = Seg (len F) by A3, FINSEQ_1:def 3;
rng G c= S

proof

let P be set ; :: 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 set such that
A5: ( k in dom G & P = G . k ) by FUNCT_1:def 5;
reconsider k = k as Element of NAT by A5;
A6: k in Seg (len F) by A3, A5, FINSEQ_1:def 3;
A7: G . k = (F . k) /\ A by A3, A5;
k in dom F by A6, FINSEQ_1:def 3;
then ( F . k in rng F & rng F c= S ) by FUNCT_1:12;
hence P in S by A5, A7, FINSUB_1:def 2; :: thesis: verum

end;

then reconsider G = G as FinSequence of S by 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 A8: ( i in dom G & j in dom G & i <> j ) ; :: thesis: G . i misses G . j
then ( i in Seg (len F) & j in Seg (len F) ) by A3, FINSEQ_1:def 3;
then ( i in dom F & j in dom F ) by FINSEQ_1:def 3;
then A9: F . i misses F . j by A8, MESFUNC3:4;
( G . i = (F . i) /\ A & G . j = (F . j) /\ A ) by A3, A8;
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 A9, XBOOLE_0:def 7 ;
hence G . i misses G . j by XBOOLE_0:def 7; :: thesis: verum

end;

then reconsider G = G as Finite_Sep_Sequence of S by MESFUNC3:4;
for v being set st v in dom (f | A) holds
v in union (rng G)

proof

let v be set ; :: 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 v in (dom f) /\ A by RELAT_1:90;
then A10: ( v in dom f & v in A ) by XBOOLE_0:def 4;
then consider W being set such that
A11: ( v in W & W in rng F ) by A1, TARSKI:def 4;
consider k being set such that
A12: ( k in dom F & W = F . k ) by A11, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A12;
A13: k in Seg (len F) by A12, FINSEQ_1:def 3;
then G . k = (F . k) /\ A by A3, A4;
then A14: v in G . k by A10, A11, A12, XBOOLE_0:def 4;
k in dom G by A3, A13, FINSEQ_1:def 3;
then G . k in rng G by FUNCT_1:12;
hence v in union (rng G) by A14, TARSKI:def 4; :: thesis: verum

end;

then A15: dom (f | A) c= union (rng G) by TARSKI:def 3;
for v being set st v in union (rng G) holds
v in dom (f | A)

proof

let v be set ; :: 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
A16: ( v in W & W in rng G ) by TARSKI:def 4;
consider k being set such that
A17: ( k in dom G & W = G . k ) by A16, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A17;
A18: k in Seg (len F) by A3, A17, FINSEQ_1:def 3;
G . k = (F . k) /\ A by A3, A17;
then A19: ( v in F . k & v in A ) by A16, A17, XBOOLE_0:def 4;
k in dom F by A18, FINSEQ_1:def 3;
then F . k in rng F by FUNCT_1:12;
then v in union (rng F) by A19, TARSKI:def 4;
then v in (dom f) /\ A by A1, A19, XBOOLE_0:def 4;
hence v in dom (f | A) by RELAT_1:90; :: thesis: verum

end;

then union (rng G) c= dom (f | A) by TARSKI:def 3;
then A20: dom (f | A) = union (rng G) by A15, XBOOLE_0:def 10;
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 A21: ( n in dom G & x in G . n & y in G . n ) ; :: thesis: (f | A) . x = (f | A) . y
then G . n in rng G by FUNCT_1:12;
then A22: ( x in dom (f | A) & y in dom (f | A) ) by A20, A21, TARSKI:def 4;
A23: n in Seg (len F) by A3, A21, FINSEQ_1:def 3;
G . n = (F . n) /\ A by A3, A21;
then A24: ( x in F . n & y in F . n ) by A21, XBOOLE_0:def 4;
n in dom F by A23, FINSEQ_1:def 3;
then f . x = f . y by A2, A24;
then (f | A) . x = f . y by A22, FUNCT_1:70;
hence (f | A) . x = (f | A) . y by A22, FUNCT_1:70; :: thesis: verum

end;

hence f | A is_simple_func_in S by A20, Def7; :: thesis: verum