let A be finite Approximation_Space; :: thesis: for x being Element of A
for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))
let x be Element of A; :: thesis: for X being disjoint_valued FinSequence of bool the carrier of A holds (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))
let X be disjoint_valued FinSequence of bool the carrier of A; :: thesis: (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X))
defpred S₁[ FinSequence of bool the carrier of A] means ( $1 is disjoint_valued implies (MemberFunc ((Union $1),A)) . x = Sum (FinSeqM (x,$1)) );
A1: for p being FinSequence of bool the carrier of A
for y being Subset of A st S₁[p] holds
S₁[p ^ <*y*>]

proof

let p be FinSequence of bool the carrier of A; :: thesis: for y being Subset of A st S₁[p] holds
S₁[p ^ <*y*>]
let y be Subset of A; :: thesis: ( S₁[p] implies S₁[p ^ <*y*>] )
assume A2: S₁[p] ; :: thesis: S₁[p ^ <*y*>]
S₁[p ^ <*y*>]

proof

assume A3: p ^ <*y*> is disjoint_valued ; :: thesis: (MemberFunc ((Union (p ^ <*y*>)),A)) . x = Sum (FinSeqM (x,(p ^ <*y*>)))
A4: Union p misses y

proof

assume Union p meets y ; :: thesis: contradiction
then consider x being set such that
A5: x in Union p and
A6: x in y by XBOOLE_0:3;
consider X being set such that
A7: x in X and
A8: X in rng p by A5, TARSKI:def 4;
consider m being set such that
A9: m in dom p and
A10: X = p . m by A8, FUNCT_1:def 5;
reconsider m = m as Element of NAT by A9;
A11: ( (p ^ <*y*>) . m = p . m & m <= len p ) by A9, FINSEQ_1:def 7, FINSEQ_3:27;
A12: ( (p ^ <*y*>) . ((len p) + 1) = y & len p < (len p) + 1 ) by FINSEQ_1:59, NAT_1:13;
p . m meets y by A6, A7, A10, XBOOLE_0:3;
hence contradiction by A3, A12, A11, PROB_2:def 3; :: thesis: verum

end;

Union (p ^ <*y*>) = (Union p) \/ (Union <*y*>) by Th5
.= (Union p) \/ y by FUNCT_6:39 ;
then (MemberFunc ((Union (p ^ <*y*>)),A)) . x = ((MemberFunc ((Union p),A)) . x) + ((MemberFunc (y,A)) . x) by A4, Th51
.= Sum ((FinSeqM (x,p)) ^ <*((MemberFunc (y,A)) . x)*>) by A2, A3, Th6, FINSEQ_6:12, RVSUM_1:104
.= Sum (FinSeqM (x,(p ^ <*y*>))) by Th53 ;
hence (MemberFunc ((Union (p ^ <*y*>)),A)) . x = Sum (FinSeqM (x,(p ^ <*y*>))) ; :: thesis: verum

end;

hence S₁[p ^ <*y*>] ; :: thesis: verum

end;

A13: S₁[ <*> (bool the carrier of A)]

proof

set F = FinSeqM (x,(<*> (bool the carrier of A)));
assume <*> (bool the carrier of A) is disjoint_valued ; :: thesis: (MemberFunc ((Union (<*> (bool the carrier of A))),A)) . x = Sum (FinSeqM (x,(<*> (bool the carrier of A))))
dom (FinSeqM (x,(<*> (bool the carrier of A)))) = dom (<*> (bool the carrier of A)) by Def10;
then A14: Sum (FinSeqM (x,(<*> (bool the carrier of A)))) = 0 by RELAT_1:64, RVSUM_1:102;
Union (<*> (bool the carrier of A)) = {} A by ZFMISC_1:2;
hence (MemberFunc ((Union (<*> (bool the carrier of A))),A)) . x = Sum (FinSeqM (x,(<*> (bool the carrier of A)))) by A14, Th54; :: thesis: verum

end;

for p being FinSequence of bool the carrier of A holds S₁[p] from FINSEQ_2:sch 2(A13, A1);
hence (MemberFunc ((Union X),A)) . x = Sum (FinSeqM (x,X)) ; :: thesis: verum