let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL
for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let f be PartFunc of X,ExtREAL; :: thesis: for F being Finite_Sep_Sequence of S
for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let F be Finite_Sep_Sequence of S; :: thesis: for a being FinSequence of ExtREAL
for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let a be FinSequence of ExtREAL ; :: thesis: for x being Element of X st F,a are_Re-presentation_of f & x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
let x be Element of X; :: thesis: ( F,a are_Re-presentation_of f & x in dom f implies ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) )
assume that
A1: F,a are_Re-presentation_of f and
A2: x in dom f ; :: thesis: ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
A3: dom F = dom a by A1;
deffunc H1( Nat) -> Element of ExtREAL = (a . $1) * ((chi ((F . $1),X)) . x);
consider ax being FinSequence of ExtREAL such that
A4: ( len ax = len a & ( for j being Nat st j in dom ax holds
ax . j = H1(j) ) ) from FINSEQ_2:sch 1();
 A5: dom ax = Seg (len a) by A4, FINSEQ_1:def 3;
A6: dom f = union (rng F) by A1;
A7: f . x = Sum ax
proof
consider Y being set such that
A8: x in Y and
A9: Y in rng F by A2, A6, TARSKI:def 4;
consider k being object such that
A10: k in dom F and
A11: Y = F . k by A9, FUNCT_1:def 3;
reconsider k = k as Element of NAT by A10;
A12: k in Seg (len a) by A3, A10, FINSEQ_1:def 3;
then A13: len ax >= k by A4, FINSEQ_1:1;
A14: for i being Nat st i in Seg (len ax) & i <> k holds
ax . i = 0.
proof
let i be Nat; :: thesis: ( i in Seg (len ax) & i <> k implies ax . i = 0. )
assume that
A15: i in Seg (len ax) and
A16: i <> k ; :: thesis: ax . i = 0.
F . i misses F . k by A16, PROB_2:def 2;
then (F . i) /\ (F . k) = {} ;
then not x in F . i by A8, A11, XBOOLE_0:def 4;
then A17: (chi ((F . i),X)) . x = 0. by FUNCT_3:def 3;
ax . i = (a . i) * ((chi ((F . i),X)) . x) by A4, A5, A15;
hence ax . i = 0. by A17; :: thesis: verum
end;
consider SA being sequence of ExtREAL such that
A18: Sum ax = SA . (len ax) and
A19: SA . 0 = 0. and
A20: for i being Nat st i < len ax holds
SA . (i + 1) = (SA . i) + (ax . (i + 1)) by EXTREAL1:def 2;
defpred S1[ Nat] means ( $1 <= len ax implies ( ( $1 < k implies SA . $1 = 0. ) & ( $1 >= k implies SA . $1 = f . x ) ) );
A21: for i being Nat st i in Seg (len ax) & i = k holds
ax . i = f . x
proof
let i be Nat; :: thesis: ( i in Seg (len ax) & i = k implies ax . i = f . x )
assume that
A22: i in Seg (len ax) and
A23: i = k ; :: thesis: ax . i = f . x
(chi ((F . i),X)) . x = 1. by A8, A11, A23, FUNCT_3:def 3;
then ax . i = (a . i) * 1. by A4, A5, A22
.= a . i by XXREAL_3:81 ;
hence ax . i = f . x by A1, A8, A10, A11, A23; :: thesis: verum
end;
A24: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A25: S1[i] ; :: thesis: S1[i + 1]
assume A26: i + 1 <= len ax ; :: thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
reconsider i = i as Element of NAT by ORDINAL1:def 12;
now :: thesis: ( ( i + 1 < k & ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) or ( i + 1 >= k & ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) )
per cases ( i + 1 < k or i + 1 >= k ) ;
case A27: i + 1 < k ; :: thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
A28: k <= len a by A12, FINSEQ_1:1;
A29: i <= i + 1 by NAT_1:11;
then i < k by A27, XXREAL_0:2;
then A30: i < len ax by A4, A28, XXREAL_0:2;
then ( 1 <= i + 1 & i + 1 <= len ax ) by NAT_1:11, NAT_1:13;
then A31: i + 1 in Seg (len ax) by FINSEQ_1:1;
SA . (i + 1) = 0. + (ax . (i + 1)) by A20, A25, A27, A29, A30, XXREAL_0:2
.= ax . (i + 1) by XXREAL_3:4
.= 0. by A14, A27, A31 ;
hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) by A27; :: thesis: verum
end;
case A32: i + 1 >= k ; :: thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
now :: thesis: ( ( k = i + 1 & SA . (i + 1) = f . x ) or ( k <> i + 1 & SA . (i + 1) = f . x ) )
per cases ( k = i + 1 or k <> i + 1 ) ;
case A33: k = i + 1 ; :: thesis: SA . (i + 1) = f . x
A34: k <= len a by A12, FINSEQ_1:1;
then i < len ax by A4, A33, NAT_1:13;
hence SA . (i + 1) = (SA . i) + (ax . (i + 1)) by A20
.= ax . k by A4, A25, A33, A34, NAT_1:13, XXREAL_3:4
.= f . x by A4, A12, A21 ;
:: thesis: verum
end;
case k <> i + 1 ; :: thesis: SA . (i + 1) = f . x
then A35: k < i + 1 by A32, XXREAL_0:1;
1 <= i + 1 by NAT_1:11;
then A36: i + 1 in Seg (len ax) by A26, FINSEQ_1:1;
i < len ax by A26, NAT_1:13;
hence SA . (i + 1) = (SA . i) + (ax . (i + 1)) by A20
.= (f . x) + 0. by A14, A25, A26, A35, A36, NAT_1:13
.= f . x by XXREAL_3:4 ;
:: thesis: verum
end;
end;
end;
hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) by A32; :: thesis: verum
end;
end;
end;
hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) ; :: thesis: verum
end;
A37: S1[ 0 ] by A12, A19, FINSEQ_1:1;
for i being Nat holds S1[i] from NAT_1:sch 2(A37, A24);
 hence f . x = Sum ax by A18, A13; :: thesis: verum
end;
take ax ; :: thesis: ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax )
dom ax = Seg (len a) by A4, FINSEQ_1:def 3;
hence ( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi ((F . n),X)) . x) ) & f . x = Sum ax ) by A4, A7, FINSEQ_1:def 3; :: thesis: verum