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 = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) ) by A1, Def1;
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;
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 )
A6: dom ax = Seg (len a) by A4, FINSEQ_1:def 3;
f . x = Sum ax
proof
consider Y being set such that
A7: ( x in Y & Y in rng F ) by A2, A3, TARSKI:def 4;
consider k being set such that
A8: ( k in dom F & Y = F . k ) by A7, FUNCT_1:def 5;
reconsider k = k as Element of NAT by A8;
A9: k in Seg (len a) by A3, A8, FINSEQ_1:def 3;
consider SA being Function of NAT ,ExtREAL such that
A10: ( Sum ax = SA . (len ax) & SA . 0 = 0. & ( for i being Element of NAT st i < len ax holds
SA . (i + 1) = (SA . i) + (ax . (i + 1)) ) ) by CONVFUN1:def 5;
A11: 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 A12: ( i in Seg (len ax) & i <> k ) ; :: thesis: ax . i = 0.
then A13: ax . i = (a . i) * ((chi (F . i),X) . x) by A4, A5;
F . i misses F . k by A12, PROB_2:def 3;
then (F . i) /\ (F . k) = {} by XBOOLE_0:def 7;
then not x in F . i by A7, A8, XBOOLE_0:def 4;
then (chi (F . i),X) . x = 0. by FUNCT_3:def 3;
hence ax . i = 0. by A13; :: thesis: verum
end;
A14: 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 A15: ( i in Seg (len ax) & i = k ) ; :: thesis: ax . i = f . x
then (chi (F . i),X) . x = 1. by A7, A8, FUNCT_3:def 3;
then ax . i = (a . i) * 1. by A4, A15, A5
.= a . i by XXREAL_3:92 ;
hence ax . i = f . x by A1, A7, A8, A15, Def1; :: thesis: verum
end;
defpred S1[ Nat] means ( $1 <= len ax implies ( ( $1 < k implies SA . $1 = 0. ) & ( $1 >= k implies SA . $1 = f . x ) ) );
A16: S1[ 0 ] by A9, A10, FINSEQ_1:3;
A17: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A18: S1[i] ; :: thesis: S1[i + 1]
assume A19: 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 13;
now
per cases ( i + 1 < k or i + 1 >= k ) ;
case A20: i + 1 < k ; :: thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
A21: i <= i + 1 by NAT_1:11;
then A22: ( i < k & i <= len ax ) by A19, A20, XXREAL_0:2;
k <= len a by A9, FINSEQ_1:3;
then A23: i < len ax by A4, A22, XXREAL_0:2;
then ( 1 <= i + 1 & i + 1 <= len ax ) by NAT_1:11, NAT_1:13;
then A24: i + 1 in Seg (len ax) by FINSEQ_1:3;
SA . (i + 1) = 0. + (ax . (i + 1)) by A10, A18, A20, A21, A23, XXREAL_0:2
.= ax . (i + 1) by XXREAL_3:4
.= 0. by A11, A20, A24 ;
hence ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) ) by A20; :: thesis: verum
end;
case A25: i + 1 >= k ; :: thesis: ( ( i + 1 < k implies SA . (i + 1) = 0. ) & ( i + 1 >= k implies SA . (i + 1) = f . x ) )
now
per cases ( k = i + 1 or k <> i + 1 ) ;
case A26: k = i + 1 ; :: thesis: SA . (i + 1) = f . x
A27: k <= len a by A9, FINSEQ_1:3;
then i < len ax by A4, A26, NAT_1:13;
hence SA . (i + 1) = (SA . i) + (ax . (i + 1)) by A10
.= ax . k by A4, A18, A26, A27, NAT_1:13, XXREAL_3:4
.= f . x by A4, A9, A14 ;
:: thesis: verum
end;
case k <> i + 1 ; :: thesis: SA . (i + 1) = f . x
then A28: k < i + 1 by A25, XXREAL_0:1;
then A29: ( k <= i & i < len ax ) by A19, NAT_1:13;
1 <= i + 1 by NAT_1:11;
then A30: i + 1 in Seg (len ax) by A19, FINSEQ_1:3;
thus SA . (i + 1) = (SA . i) + (ax . (i + 1)) by A10, A29
.= (f . x) + 0. by A11, A18, A19, A28, A30, 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 A25; :: 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;
A31: for i being Nat holds S1[i] from NAT_1:sch 2(A16, A17);
 len ax >= k by A4, A9, FINSEQ_1:3;
hence f . x = Sum ax by A10, A31; :: thesis: verum
end;
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, A6, FINSEQ_1:def 3; :: thesis: verum