let I be set ; :: thesis: for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|
let M be ManySortedSet of I; :: 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 I ;
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 object st i in I holds
(MSUnion A) . i = UA . i
proof
let i be object ; :: thesis: ( i in I implies (MSUnion A) . i = UA . i )
assume A2: i in I ; :: thesis: (MSUnion A) . i = UA . i
then ( |:A:| . i = { (g . i) where g is Element of Bool M : g in A } & UA . i = union (|:A:| . i) ) by A1, CLOSURE2:14, MBOOLEAN:def 2;
hence (MSUnion A) . i = UA . i by A2, Def2; :: thesis: verum
end;
hence MSUnion A = union |:A:| ; :: thesis: verum
end;
suppose A3: A is empty SubsetFamily of M ; :: thesis: MSUnion A = union |:A:|
for i being object st i in I holds
(MSUnion A) . i = UA . i
proof
let i be object ; :: thesis: ( i in I implies (MSUnion A) . i = UA . i )
assume i in I ; :: thesis: (MSUnion A) . i = UA . i
|:A:| = EmptyMS I by A3;
then UA = EmptyMS I by MBOOLEAN:21;
then UA . i is empty ;
hence (MSUnion A) . i = UA . i by A3; :: thesis: verum
end;
hence MSUnion A = union |:A:| ; :: thesis: verum
end;
end;