let X be non empty set ; :: thesis: for S being non empty Subset-Family of X
for f being FinSequence of S
for F being FinSequence of PFuncs (X,ExtREAL) st dom f = dom F & f is disjoint_valued & ( for n being Nat st n in dom F holds
F . n = chi ((f . n),X) ) holds
for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x)
let S be non empty Subset-Family of X; :: thesis: for f being FinSequence of S
for F being FinSequence of PFuncs (X,ExtREAL) st dom f = dom F & f is disjoint_valued & ( for n being Nat st n in dom F holds
F . n = chi ((f . n),X) ) holds
for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x)
let f be FinSequence of S; :: thesis: for F being FinSequence of PFuncs (X,ExtREAL) st dom f = dom F & f is disjoint_valued & ( for n being Nat st n in dom F holds
F . n = chi ((f . n),X) ) holds
for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x)
let F be FinSequence of PFuncs (X,ExtREAL); :: thesis: ( dom f = dom F & f is disjoint_valued & ( for n being Nat st n in dom F holds
F . n = chi ((f . n),X) ) implies for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x) )
assume that
A0: dom f = dom F and
A1: f is disjoint_valued and
A2: for n being Nat st n in dom F holds
F . n = chi ((f . n),X) ; :: thesis: for x being Element of X holds (chi ((Union f),X)) . x = Sum (F # x)
let x be Element of X; :: thesis: (chi ((Union f),X)) . x = Sum (F # x)
reconsider x1 = x as Element of X ;
consider Sf being sequence of ExtREAL such that
B1: ( Sum (F # x) = Sf . (len (F # x)) & Sf . 0 = 0 & ( for i being Nat st i < len (F # x) holds
Sf . (i + 1) = (Sf . i) + ((F # x) . (i + 1)) ) ) by EXTREAL1:def 2;
per cases ( x in Union f or not x in Union f ) ;
suppose A8: x in Union f ; :: thesis: (chi ((Union f),X)) . x = Sum (F # x)
then x in union (rng f) by CARD_3:def 4;
then consider fn being set such that
A9: ( x in fn & fn in rng f ) by TARSKI:def 4;
consider n being Element of NAT such that
A10: ( n in dom f & fn = f . n ) by A9, PARTFUN1:3;
A11: for m being Nat holds
( ( m = n implies (F # x) . m = 1 ) & ( m <> n implies (F # x) . m = 0 ) )
proof
let m be Nat; :: thesis: ( ( m = n implies (F # x) . m = 1 ) & ( m <> n implies (F # x) . m = 0 ) )
hereby :: thesis: ( m <> n implies (F # x) . m = 0 )
assume A12: m = n ; :: thesis: (F # x) . m = 1
then m in dom (F # x) by A0, A10, DEF5;
then (F # x) . m = (F . m) . x by DEF5;
then (F # x) . m = (chi ((f . m),X)) . x by A2, A12, A10, A0;
hence (F # x) . m = 1 by A9, A10, A12, FUNCT_3:def 3; :: thesis: verum
end;
assume m <> n ; :: thesis: (F # x) . m = 0
then A13: not x in f . m by A9, A10, A1, PROB_2:def 2, XBOOLE_0:3;
per cases ( m in dom (F # x) or not m in dom (F # x) ) ;
suppose m in dom (F # x) ; :: thesis: (F # x) . m = 0
then ( m in dom F & (F # x) . m = (F . m) . x ) by DEF5;
then (F # x) . m = (chi ((f . m),X)) . x by A2;
hence (F # x) . m = 0 by A13, FUNCT_3:def 3; :: thesis: verum
end;
suppose not m in dom (F # x) ; :: thesis: (F # x) . m = 0
hence (F # x) . m = 0 by FUNCT_1:def 2; :: thesis: verum
end;
end;
end;
defpred S1[ Nat] means ( $1 < n implies Sf . $1 = 0 );
A14: S1[ 0 ] by B1;
A15: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A16: S1[m] ; :: thesis: S1[m + 1]
assume A17: m + 1 < n ; :: thesis: Sf . (m + 1) = 0
then A18: m < n by NAT_1:13;
A20: (F # x) . (m + 1) = 0 by A17, A11;
n in dom (F # x) by A0, A10, DEF5;
then ( 1 <= n & n <= len (F # x) ) by FINSEQ_3:25;
then m < len (F # x) by A18, XXREAL_0:2;
then Sf . (m + 1) = (Sf . m) + ((F # x) . (m + 1)) by B1
.= 0 + 0 by A20, A16, A17, NAT_1:13 ;
hence Sf . (m + 1) = 0 ; :: thesis: verum
end;
A21: for m being Nat holds S1[m] from NAT_1:sch 2(A14, A15);
defpred S2[ Nat] means ( n <= $1 & $1 <= len (F # x) implies Sf . $1 = 1 );
A23: S2[ 0 ] by A10, FINSEQ_3:25;
A24: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A25: S2[m] ; :: thesis: S2[m + 1]
assume A26: ( n <= m + 1 & m + 1 <= len (F # x) ) ; :: thesis: Sf . (m + 1) = 1
then A27: Sf . (m + 1) = (Sf . m) + ((F # x) . (m + 1)) by B1, NAT_1:13;
per cases ( n = m + 1 or n < m + 1 ) by A26, XXREAL_0:1;
suppose A28: n = m + 1 ; :: thesis: Sf . (m + 1) = 1
then m < n by NAT_1:13;
then ( Sf . m = 0 & (F # x) . (m + 1) = 1 ) by A21, A28, A11;
hence Sf . (m + 1) = 1 by A27, XXREAL_3:4; :: thesis: verum
end;
suppose n < m + 1 ; :: thesis: Sf . (m + 1) = 1
then ( Sf . m = 1 & (F # x) . (m + 1) = 0 ) by A25, A11, A26, NAT_1:13;
hence Sf . (m + 1) = 1 by A27, XXREAL_3:4; :: thesis: verum
end;
end;
end;
A30: for m being Nat holds S2[m] from NAT_1:sch 2(A23, A24);
 n in dom (F # x) by A10, A0, DEF5;
then n <= len (F # x) by FINSEQ_3:25;
then Sf . (len (F # x)) = 1 by A30;
hence (chi ((Union f),X)) . x = Sum (F # x) by A8, B1, FUNCT_3:def 3; :: thesis: verum
end;
suppose A31: not x in Union f ; :: thesis: (chi ((Union f),X)) . x = Sum (F # x)
then not x in union (rng f) by CARD_3:def 4;
then A32: for V being set st V in rng f holds
not x in V by TARSKI:def 4;
defpred S1[ Nat] means ( $1 <= len (F # x) implies Sf . $1 = 0 );
A33: S1[ 0 ] by B1;
A34: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A35: S1[m] ; :: thesis: S1[m + 1]
assume A37: m + 1 <= len (F # x) ; :: thesis: Sf . (m + 1) = 0
then A38: m + 1 in dom (F # x) by NAT_1:11, FINSEQ_3:25;
then C2: m + 1 in dom f by A0, DEF5;
then A39: not x in f . (m + 1) by A32, FUNCT_1:3;
(F # x) . (m + 1) = (F . (m + 1)) . x by A38, DEF5
.= (chi ((f . (m + 1)),X)) . x by A2, C2, A0 ;
then (F # x) . (m + 1) = 0 by A39, FUNCT_3:def 3;
then (Sf . m) + ((F # x) . (m + 1)) = 0 by A35, A37, NAT_1:13;
hence Sf . (m + 1) = 0 by A37, B1, NAT_1:13; :: thesis: verum
end;
for m being Nat holds S1[m] from NAT_1:sch 2(A33, A34);
then Sum (F # x) = 0 by B1;
hence (chi ((Union f),X)) . x = Sum (F # x) by A31, FUNCT_3:def 3; :: thesis: verum
end;
end;