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;

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

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

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)

then A12:
union (rng G) c= dom (f | A)
;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;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

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

(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;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 object st x in G . k holds
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;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

(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

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

v in union (rng G)

then
dom (f | A) c= union (rng G)
;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;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

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