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 ;

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 )
;

end;

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

end;(MSUnion A) . i = UA . i

proof

hence
MSUnion A = union |:A:|
; :: thesis: verum
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;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

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

end;(MSUnion A) . i = UA . i

proof

hence
MSUnion A = union |:A:|
; :: thesis: verum
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;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