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

now

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 A4: ( v in dom f & v in A ) by XBOOLE_0:def 4;
then v in union (rng F) by A3, MESFUNC3:def 1;
then consider C being set such that
A5: ( v in C & C in rng F ) by TARSKI:def 4;
consider k being Nat such that
A6: ( k in dom F & C = F . k ) by A5, FINSEQ_2:11;
A7: G . k = (F . k) /\ A by A2, A6;
A8: G . k in rng G by A1, A6, FUNCT_1:12;
v in (F . k) /\ A by A4, A5, A6, XBOOLE_0:def 4;
hence v in union (rng G) by A7, A8, TARSKI:def 4; :: thesis: verum

end;

then A9: dom (f | A) c= union (rng G) by TARSKI:def 3;

now

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 C being set such that
A10: ( v in C & C in rng G ) by TARSKI:def 4;
consider k being set such that
A11: ( k in dom G & C = G . k ) by A10, FUNCT_1:def 5;
G . k = (F . k) /\ A by A1, A2, A11;
then A12: ( v in F . k & v in A ) by A10, A11, XBOOLE_0:def 4;
F . k in rng F by A1, A11, FUNCT_1:12;
then v in union (rng F) by A12, TARSKI:def 4;
then v in dom f by A3, MESFUNC3:def 1;
then v in (dom f) /\ A by A12, XBOOLE_0:def 4;
hence v in dom (f | A) by RELAT_1:90; :: thesis: verum

end;

then A13: union (rng G) c= dom (f | A) by TARSKI:def 3;
then A14: dom (f | A) = union (rng G) by A9, XBOOLE_0:def 10;
A15: dom G = dom a by A1, A3, MESFUNC3:def 1;
for k being Nat st k in dom G holds
for x being set st x in G . k holds
(f | A) . 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 | A) . x = a . k )
assume A16: k in dom G ; :: thesis: for x being set st x in G . k holds
(f | A) . x = a . k
let x be set ; :: 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:12;
then x in union (rng G) by A17, TARSKI:def 4;
then A18: (f | A) . x = f . x by A13, FUNCT_1:70;
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 A19: 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, A19;
then x in F . k by XBOOLE_0:def 4;
hence f . x = a . k by A1, A3, A19, MESFUNC3:def 1; :: thesis: verum

end;

hence (f | A) . x = a . k by A16, A17, A18; :: thesis: verum

end;

hence G,a are_Re-presentation_of f | A by A14, A15, MESFUNC3:def 1; :: thesis: verum