let I be set ; :: thesis: for M being ManySortedSet of
for A being SubsetFamily of M holds MSUnion A = union |:A:|
let M be ManySortedSet of ; :: thesis: for A being SubsetFamily of M holds MSUnion A = union |:A:|
let A be SubsetFamily of M; :: thesis: MSUnion A = union |:A:|
set AA = |:A:|;
reconsider UA = union |:A:| as ManySortedSet of ;

per cases ( not A is empty or A is empty SubsetFamily of M ) ;

suppose A1: not A is empty ; :: thesis: MSUnion A = union |:A:|

for i being set st i in I holds
(MSUnion A) . i = UA . i

proof

let i be set ; :: thesis: ( i in I implies (MSUnion A) . i = UA . i )
assume A2: i in I ; :: thesis: (MSUnion A) . i = UA . i
then A3: |:A:| . i = { (g . i) where g is Element of Bool M : g in A } by A1, CLOSURE2:15;
UA . i = union (|:A:| . i) by A2, MBOOLEAN:def 2;
hence (MSUnion A) . i = UA . i by A2, A3, Def4; :: thesis: verum

end;

hence MSUnion A = union |:A:| by PBOOLE:3; :: thesis: verum

end;

suppose A4: A is empty SubsetFamily of M ; :: thesis: MSUnion A = union |:A:|

A5: MSUnion A is empty-yielding by A4;
for i being set st i in I holds
(MSUnion A) . i = UA . i

proof

let i be set ; :: thesis: ( i in I implies (MSUnion A) . i = UA . i )
assume A6: i in I ; :: thesis: (MSUnion A) . i = UA . i
|:A:| = [0] I by A4, CLOSURE2:def 4;
then UA = [0] I by MBOOLEAN:22;
then UA . i is empty by A6, PBOOLE:def 15;
hence (MSUnion A) . i = UA . i by A5, A6, PBOOLE:def 15; :: thesis: verum

end;

hence MSUnion A = union |:A:| by PBOOLE:3; :: thesis: verum

end;

end;