let I be set ; :: thesis: for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)
let M be ManySortedSet of I; :: thesis: for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)
let A, B be SubsetFamily of M; :: thesis: MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B)
reconsider MAB = MSUnion (A \/ B) as ManySortedSubset of M ;
reconsider MAB = MAB as ManySortedSet of I ;
reconsider MA = MSUnion A as ManySortedSubset of M ;
reconsider MA = MA as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSubset of M ;
reconsider MB = MB as ManySortedSet of I ;
for i being object st i in I holds
MAB . i = (MA (\/) MB) . i

proof

let i be object ; :: thesis: ( i in I implies MAB . i = (MA (\/) MB) . i )
assume A1: i in I ; :: thesis: MAB . i = (MA (\/) MB) . i
then A2: MAB . i = union { (f . i) where f is Element of Bool M : f in A \/ B } by Def2;
A3: (MA (\/) MB) . i = (MA . i) \/ (MB . i) by A1, PBOOLE:def 4;
A4: for v being object st v in (MA (\/) MB) . i holds
v in MAB . i

proof

let v be object ; :: thesis: ( v in (MA (\/) MB) . i implies v in MAB . i )
assume v in (MA (\/) MB) . i ; :: thesis: v in MAB . i
then A5: ( v in MA . i or v in MB . i ) by A3, XBOOLE_0:def 3;

per cases ( v in union { (f . i) where f is Element of Bool M : f in A } or v in union { (f . i) where f is Element of Bool M : f in B } ) by A1, A5, Def2;

suppose v in union { (f . i) where f is Element of Bool M : f in A } ; :: thesis: v in MAB . i

then consider g being set such that
A6: v in g and
A7: g in { (f . i) where f is Element of Bool M : f in A } by TARSKI:def 4;
consider h being Element of Bool M such that
A8: g = h . i and
A9: h in A by A7;
h in A \/ B by A9, XBOOLE_0:def 3;
then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A8;
hence v in MAB . i by A2, A6, TARSKI:def 4; :: thesis: verum

end;

suppose v in union { (f . i) where f is Element of Bool M : f in B } ; :: thesis: v in MAB . i

then consider g being set such that
A10: v in g and
A11: g in { (f . i) where f is Element of Bool M : f in B } by TARSKI:def 4;
consider h being Element of Bool M such that
A12: g = h . i and
A13: h in B by A11;
h in A \/ B by A13, XBOOLE_0:def 3;
then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A12;
hence v in MAB . i by A2, A10, TARSKI:def 4; :: thesis: verum

end;

end;

end;

A14: ( MA . i = union { (f . i) where f is Element of Bool M : f in A } & MB . i = union { (f . i) where f is Element of Bool M : f in B } ) by A1, Def2;
for v being object st v in MAB . i holds
v in (MA (\/) MB) . i

proof

let v be object ; :: thesis: ( v in MAB . i implies v in (MA (\/) MB) . i )
assume v in MAB . i ; :: thesis: v in (MA (\/) MB) . i
then consider h being set such that
A15: v in h and
A16: h in { (f . i) where f is Element of Bool M : f in A \/ B } by A2, TARSKI:def 4;
consider g being Element of Bool M such that
A17: h = g . i and
A18: g in A \/ B by A16;
( g in A or g in B ) by A18, XBOOLE_0:def 3;
then ( h in { (f . i) where f is Element of Bool M : f in A } or h in { (f . i) where f is Element of Bool M : f in B } ) by A17;
then ( v in union { (f . i) where f is Element of Bool M : f in A } or v in union { (f . i) where f is Element of Bool M : f in B } ) by A15, TARSKI:def 4;
hence v in (MA (\/) MB) . i by A3, A14, XBOOLE_0:def 3; :: thesis: verum

end;

hence MAB . i = (MA (\/) MB) . i by A4, TARSKI:2; :: thesis: verum

end;

hence MSUnion (A \/ B) = (MSUnion A) (\/) (MSUnion B) ; :: thesis: verum