let X be non empty set ; 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; 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; 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; 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; 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 ; ( 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
; G,a are_Re-presentation_of f | A
A4:
dom G = dom a
by A1, A3, MESFUNC3:def 1;
now for v being object st v in union (rng G) holds
v in dom (f | A)let v be
object ;
( v in union (rng G) implies v in dom (f | A) )assume
v in union (rng G)
;
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;
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
now for v being object st v in dom (f | A) holds
v in union (rng G)let v be
object ;
( v in dom (f | A) implies v in union (rng G) )assume
v in dom (f | A)
;
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;
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; verum