let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for A being Element of S
for F, G being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL st dom F = dom G & ( for n being Nat st n in dom F holds
G . n = (F . n) /\ A ) & F,a are_Re-presentation_of f holds
G,a are_Re-presentation_of f | A
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S
for F, G being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL st dom F = dom G & ( for n being Nat st n in dom F holds
G . n = (F . n) /\ A ) & F,a are_Re-presentation_of f holds
G,a are_Re-presentation_of f | A
let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S
for F, G being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL st dom F = dom G & ( for n being Nat st n in dom F holds
G . n = (F . n) /\ A ) & F,a are_Re-presentation_of f holds
G,a are_Re-presentation_of f | A
let A be Element of S; :: thesis: for F, G being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL st dom F = dom G & ( for n being Nat st n in dom F holds
G . n = (F . n) /\ A ) & F,a are_Re-presentation_of f holds
G,a are_Re-presentation_of f | A
let F, G be Finite_Sep_Sequence of S; :: thesis: for a being FinSequence of ExtREAL st dom F = dom G & ( for n being Nat st n in dom F holds
G . n = (F . n) /\ A ) & F,a are_Re-presentation_of f holds
G,a are_Re-presentation_of f | A
let a be FinSequence of ExtREAL ; :: thesis: ( dom F = dom G & ( for n being Nat st n in dom F holds
G . n = (F . n) /\ A ) & F,a are_Re-presentation_of f implies G,a are_Re-presentation_of f | A )
assume that
A1: dom F = dom G and
A2: for n being Nat st n in dom F holds
G . n = (F . n) /\ A and
A3: F,a are_Re-presentation_of f ; :: thesis: G,a are_Re-presentation_of f | A
A4: dom G = dom a by A1, A3, MESFUNC3:def 1;

now :: thesis: for v being object st v in union (rng G) holds
v in dom (f | A)

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 C being set such that
A5: v in C and
A6: C in rng G by TARSKI:def 4;
consider k being object such that
A7: k in dom G and
A8: C = G . k by A6, FUNCT_1:def 3;
A9: F . k in rng F by A1, A7, FUNCT_1:3;
A10: G . k = (F . k) /\ A by A1, A2, A7;
then v in F . k by A5, A8, XBOOLE_0:def 4;
then v in union (rng F) by A9, TARSKI:def 4;
then A11: v in dom f by A3, MESFUNC3:def 1;
v in A by A5, A8, A10, XBOOLE_0:def 4;
then v in (dom f) /\ A by A11, XBOOLE_0:def 4;
hence v in dom (f | A) by RELAT_1:61; :: thesis: verum

end;

then A12: union (rng G) c= dom (f | A) ;
A13: for k being Nat st k in dom G holds
for x being object st x in G . k holds
(f | A) . x = a . k

proof

A14: for k being Nat st k in dom G holds
for x being set st x in G . k holds
f . x = a . k

proof

let k be Nat; :: thesis: ( k in dom G implies for x being set st x in G . k holds
f . x = a . k )
assume A15: k in dom G ; :: thesis: for x being set st x in G . k holds
f . x = a . k
let x be set ; :: thesis: ( x in G . k implies f . x = a . k )
assume x in G . k ; :: thesis: f . x = a . k
then x in (F . k) /\ A by A1, A2, A15;
then x in F . k by XBOOLE_0:def 4;
hence f . x = a . k by A1, A3, A15, MESFUNC3:def 1; :: thesis: verum

end;

let k be Nat; :: thesis: ( k in dom G implies for x being object st x in G . k holds
(f | A) . x = a . k )
assume A16: k in dom G ; :: thesis: for x being object st x in G . k holds
(f | A) . x = a . k
let x be object ; :: thesis: ( x in G . k implies (f | A) . x = a . k )
assume A17: x in G . k ; :: thesis: (f | A) . x = a . k
G . k in rng G by A16, FUNCT_1:3;
then x in union (rng G) by A17, TARSKI:def 4;
then (f | A) . x = f . x by A12, FUNCT_1:47;
hence (f | A) . x = a . k by A16, A17, A14; :: thesis: verum

end;

now :: thesis: for v being object st v in dom (f | A) holds
v in union (rng G)

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 A18: v in (dom f) /\ A by RELAT_1:61;
then v in dom f by XBOOLE_0:def 4;
then v in union (rng F) by A3, MESFUNC3:def 1;
then consider C being set such that
A19: v in C and
A20: C in rng F by TARSKI:def 4;
consider k being Nat such that
A21: k in dom F and
A22: C = F . k by A20, FINSEQ_2:10;
A23: G . k = (F . k) /\ A by A2, A21;
A24: G . k in rng G by A1, A21, FUNCT_1:3;
v in A by A18, XBOOLE_0:def 4;
then v in (F . k) /\ A by A19, A22, XBOOLE_0:def 4;
hence v in union (rng G) by A23, A24, TARSKI:def 4; :: thesis: verum

end;

then dom (f | A) c= union (rng G) ;
then dom (f | A) = union (rng G) by A12;
hence G,a are_Re-presentation_of f | A by A4, A13, MESFUNC3:def 1; :: thesis: verum